|
Universe i j.
Goal False.
Proof.
Check Type@{i} : Type@{j}.
Fail constr_eq_strict Type@{i} Type@{j}.
assert_succeeds constr_eq Type@{i} Type@{j}. (* <- i=j is forgotten after assert_succeeds *)
Fail constr_eq_strict Type@{i} Type@{j}.
constr_eq Type@{i} Type@{j}. (* <- i=j is retained *)
constr_eq_strict Type@{i} Type@{j}.
Fail Check Type@{i} : Type@{j}.
Fail constr_eq Prop Set.
Fail constr_eq Prop Type.
Fail constr_eq_strict Type Type.
constr_eq Type Type.
constr_eq_strict Set Set.
constr_eq Set Set.
constr_eq Prop Prop.
let x := constr:(Type) in constr_eq_strict x x.
let x := constr:(Type) in constr_eq x x.
Fail lazymatch type of prod with
| ?A -> ?B -> _ => constr_eq_strict A B
end.
lazymatch type of prod with
| ?A -> ?B -> _ => constr_eq A B
end.
lazymatch type of prod with
| ?A -> ?B -> ?C => constr_eq A C
end.
Abort.
¤ Dauer der Verarbeitung: 0.18 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.
|
