#[export] Instance foo1 (a : nat) {b : nat} (e : a = b) : True := I. Check foo1 (a := 3) (b := 4).
Definition foo2 (a : nat) {b : nat} (e : a = b) : True := I. Check foo2 (a := 3) (b := 4).
#[export] Instance foo3 (a : nat) {b : nat} (e : a = b) : True. exact I. Qed. Check foo3 (a := 3) (b := 4).
Messung V0.5 in Prozent
¤ 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.0Bemerkung:
(vorverarbeitet am 2026-09-30)
¤
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.