(* An example showing that prop-extensionality is incompatible with powerful extensions of the guard condition. This is a variation on the example in subterm2, exploiting missing typing constraints in the commutative cut subterm rule (subterm2 is using the same flaw but for the match rule).
Fail Fixpoint loop (x : True2) : False := match x with
I3 f => (match T3F_FT3F in _=T return T with eq_refl=> loop end) f end.
Messung V0.5
¤ 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.0.10Bemerkung:
(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 und die Messung sind noch experimentell.
