|
Inductive comp : Type -> Type :=
| Ret {T} : forall (v:T), comp T
| Bind {T T'} : forall (p: comp T') (p': T' -> comp T), comp T.
Notation "'do' x .. y <- p1 ; p2" :=
(Bind p1 (fun x => .. (fun y => p2) ..))
(at level 60, right associativity,
x binder, y binder).
Definition Fst1 A B (p: comp (A*B)) : comp A :=
do '(a, b) <- p;
Ret a.
Definition Fst2 A B (p: comp (A*B)) : comp A :=
match tt with
| _ => Bind p (fun '(a, b) => Ret a)
end.
Definition Fst3 A B (p: comp (A*B)) : comp A :=
match tt with
| _ => do a <- p;
Ret (fst a)
end.
Definition Fst A B (p: comp (A * B)) : comp A :=
match tt with
| _ => do '(a, b) <- p;
Ret a
end.
¤ Dauer der Verarbeitung: 0.16 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.
|
