| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Roqc/test-suite/success/ (Beweissystem des Inria Version 9.1.0©) Datei vom 15.8.2025 mit Größe 595 B |
|
Quelle eta.v Sprache: Coq |
|||||||||||||||
|
(* 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.2 Sekunden ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-04-04