|
(* 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.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.
|
