(* 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.
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.
