Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Delphi/Agenda 1.1/   (Columbo Version 0.7©)  Datei vom 4.1.2008 mit Größe 98 B image not shown  

Quellcode-Bibliothek bug_12529.v   Sprache: unbekannt

 
Goal SProp.
match goal with |- SProp => idtac end.
Fail match goal with |- Prop => idtac end.
Abort.

Goal Prop.
Fail match goal with |- SProp => idtac end.
match goal with |- Prop => idtac end.
Abort.

Class F A := f : A.

Inductive pFalse : Prop  := .
Inductive sFalse : SProp := .

#[export] Hint Extern 0 (F Prop) => exact pFalse : typeclass_instances.
Definition pf := f : Prop.

#[export] Hint Extern 0 (F SProp) => exact sFalse : typeclass_instances.
Definition sf := (f : SProp).
Definition pf' := (f : Prop).

100%


[ 0.21Quellennavigators  Projekt   ]