products/sources/formale Sprachen/Cobol/Test-Suite/SQL M/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: case_polyuniv.v   Sprache: Unknown

Require Import ssreflect.

Set Universe Polymorphism.

Cumulative Variant paths {A} (x:A) : A -> Type
  := idpath : paths x x.

Register paths as core.eq.type.
Register idpath as core.eq.refl.

Lemma case_test (b:bool) : paths b b.
Proof. case B:b; reflexivity. Qed.

[ Dauer der Verarbeitung: 0.0 Sekunden  (vorverarbeitet)  ]