Set Primitive Projections. Class Foo (F : False) := { foo : True }. Arguments foo F {Foo}. PrintImplicit foo. (* foo : forall F : False, Foo F -> True
Argument Foo is implicit and maximally inserted *) Check foo _. (* Toplevel input, characters 6-11: Error: Illegal application (Non-functional construction): The expression "foo" of type "True" cannot be applied to the term
"?36" : "?35" *)
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
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.
