Quelle bug_4932.v Sprache: 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.

quality100%

¤ Dauer der Verarbeitung: 0.4 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.