Set Printing All. Definition foo (s d : Prop)
: ((s : Set) -> (d : Set)) = ((s : Prop) -> (d : Prop))
:= eq_refl. (* succeeds *) Definition bar (s d : Prop)
: ((fun x : Set => x) s -> (fun x : Set => x) d) = ((fun x : Prop => x) s -> (fun x : Prop => x) d)
:= eq_refl. (* Toplevel input, characters 131-138: Error: In environment s : Prop d : Prop The term "@eq_refl Set (forall _ : (fun x : Set => x) s, (fun x : Set => x) d)" has type "@eq Set (forall _ : s, d) (forall _ : s, d)" while it is expected to have type "@eq Set (forall _ : s, d) (forall _ : s, d)" (cannot unify "forall _ : (fun x : Set => x) s, (fun x : Set => x) d" and
"forall _ : (fun x : Prop => x) s, (fun x : Prop => x) d"). *)
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.
