|
(* Test maximal implicit arguments in the presence of let-ins *)
Definition foo (x := 1) {y : nat} (H : y = y) : True := I.
Definition bar {y : nat} (x := 1) (H : y = y) : True := I.
Check bar (eq_refl 1).
Check foo (eq_refl 1).
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
