(* There used to be an evar leak in the to_nat example *)
Fixpoint Idx {A:Type} (l:list A) : Type := match l with
| nil => False
| cons _ l => True + Idx l end.
Fixpoint to_nat {A:Type} (l:list A) (i:Idx l) : nat := match l,i with
| nil , i => match i withend
| cons _ _, inl _ => 0
| cons _ l, inr i => S (to_nat l i) end.
Messung V0.5
¤ Dauer der Verarbeitung: 0.10 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 und die Messung sind noch experimentell.
