Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: bug_4787.v Sprache: Coq

Original von: Coq^©

(* Testing recursive notations with binders seen as terms *)

Inductive ftele : Type :=
| fb {T:Type} : T -> ftele
| fr {T} : (T -> ftele) -> ftele.

Fixpoint args ftele : Type :=
  match ftele with
    | fb _ => unit
    | fr f => sigT (fun t => args (f t))
  end.

Definition fpack := sigT args.
Definition pack fp fa : fpack := existT _ fp fa.

Notation "'tele' x .. z := b" :=
  (
    (fun x => ..
                (fun z =>
                   pack
                     (fr (fun x => .. ( fr (fun z => fb b) ) .. ) )
                     (existT _ x .. (existT _ z tt) .. )
                ) ..
    )
  ) (at level 85, x binder, z binder).

Check fun '((y,z):nat*nat) => pack (fr (fun '((y,z):nat*nat) => fb tt))
                                   (existT _ (y,z) tt).

Example test := tele (t : Type) := tt.
Example test' := test nat.
Print test.

Example test2 := tele (t : Type) (x:t) := tt.
Example test2' := test2 nat 0.
Print test2.

Example test3 := tele (t : Type) (y:=0) (x:t) := tt.
Example test3' := test3 nat 0.
Print test3.

Example test4 := tele (t : Type) '((y,z):nat*nat) (x:t) := tt.
Example test4' := test4 nat (1,2) 3.
Print test4.

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.