products/Sources/formale Sprachen/Coq/test-suite/bugs/opened/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: sq110m.cob   Sprache: Coq

Original von: Coq©
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.2 Sekunden  (vorverarbeitet)  ¤



Druckansicht
unsichere Verbindung
Druckansicht
sprechenden Kalenders

Eigene Datei ansehen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff