|
(* Kernel test (head term is a constant) *)
Check (fun a : S = S => a : S = fun x => S x).
(* Kernel test (head term is a variable) *)
Check (fun (f:nat->nat) (a : f = f) => a : f = fun x => f x).
(* Test type inference (head term is syntactically rigid) *)
Check (fun (a : list = list) => a : list = fun A => _ A).
(* Test type inference (head term is a variable) *)
(* This one is still to be done...
Check (fun (f:nat->nat) (a : f = f) => a : f = fun x => _ x).
*)
(* Test tactic unification *)
Goal (forall f:nat->nat, (fun x => f x) = (fun x => f x)) -> S = S.
intro H; apply H.
Qed.
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
