|
(* An example of type inference *)
Axiom A : Type.
Definition f (x y : A) := x.
Axiom g : forall x y : A, f x y = y -> Prop.
Axiom x : A.
Check (g x _ (refl_equal x)).
¤ Dauer der Verarbeitung: 0.14 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.
|
