|
(* There used to be an evar leak in the to_nat example *)
Require Import Coq.Lists.List.
Import ListNotations.
Fixpoint Idx {A:Type} (l:list A) : Type :=
match l with
| [] => False
| _::l => True + Idx l
end.
Fixpoint to_nat {A:Type} (l:list A) (i:Idx l) : nat :=
match l,i with
| [] , i => match i with end
| _::_, inl _ => 0
| _::l, inr i => S (to_nat l i)
end.
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
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.
|
