Permalink
Switch branches/tags
Nothing to show
Find file
Fetching contributors…
Cannot retrieve contributors at this time
34 lines (29 sloc) 894 Bytes
(** This file defines the syntax of the System T extended with stream types. *)
(* Types *)
Inductive ty :=
| tbool : ty
| tnat : ty
| tarrow : ty -> ty -> ty
| stream : ty -> ty.
Notation " A '→' B " := (tarrow A B) (at level 30, right associativity) : t_scope.
Notation " 'ω' " := tnat : t_scope.
Notation " '2' " := tbool : t_scope.
Open Scope t_scope.
(* Terms *)
(* The formalisation uses de Bruijn indices to deal with binders. *)
Inductive te :=
| var : nat -> te
| lam : ty -> te -> te
| appl : te -> te -> te
| z : te
| s : te -> te
| rec : te -> te -> te -> te
| hd : te -> te
| tl : te -> te
| seed : te -> te -> te -> te
| TT : te
| FF : te.
Notation "'λ' A , M " := (lam A M) (at level 50) : t_scope.
Notation " # n " := (var n) (at level 20) : t_scope.
Notation " M @ N " := (appl M N) (at level 40, left associativity) : t_scope.
Close Scope t_scope.