Ltac2 good_1(o: 'a option) := match o with
| Some x => 1
| None => 2 end.
Ltac2 good_2(o: 'a option) := match o with
| Some x => 1
| _ => 2 end.
Fail Ltac2 redundant_constructor(o: 'a option) := match o with
| Some x => 1
| None => 2
| Some y => 3 end.
Fail Ltac2 redundant_catch_all(o: 'a option) := match o with
| Some x => 1
| None => 2
| _ => 3 end.
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.11Bemerkung:
(vorverarbeitet am 2026-09-29)
¤
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.