setup coq project & initial definition of terms (types & expressions)

.gitignore

@@ -0,0 +1,6 @@
+*.glob
+*.vo
+*.vok
+*.vos
+*.aux
+*.pdf

coq/_CoqProject

@@ -0,0 +1,8 @@
+-R . LadderTypes
+terms.v
+equiv.v
+subst.v
+typing.v
+smallstep.v
+bbencode.v
+

coq/terms.v

@@ -0,0 +1,44 @@
+(* Define the abstract syntax of the calculus
+ * by inductive definition of type-terms
+ * and expression-terms.
+ *)
+
+From Coq Require Import Strings.String.
+Module Terms.
+
+(* types *)
+Inductive ladder_type : Type :=
+  | type_unit : ladder_type
+  | type_id : string -> ladder_type
+  | type_var : string -> ladder_type
+  | type_num : nat -> ladder_type
+  | type_abs : string -> ladder_type -> ladder_type
+  | type_app : ladder_type -> ladder_type -> ladder_type
+  | type_fun : ladder_type -> ladder_type -> ladder_type
+  | type_rung : ladder_type -> ladder_type -> ladder_type
+.
+
+(* expressions *)
+Inductive expr : Type :=
+  | expr_var : string -> expr
+  | expr_ty_abs : string -> expr -> expr
+  | expr_ty_app : expr -> ladder_type -> expr
+  | expr_tm_abs : string -> ladder_type -> expr -> expr
+  | expr_tm_app : expr -> expr -> expr
+  | expr_let : string -> ladder_type -> expr -> expr -> expr
+  | expr_ascend : ladder_type -> expr -> expr
+  | expr_descend : ladder_type -> expr -> expr
+.
+
+Coercion type_var : string >-> ladder_type.
+Coercion expr_var : string >-> expr.
+
+
+(*
+Notation "( x )" := x (at level 70).
+Notation "x ~ y" := (type_rung x y) (at level 69, left associativity).
+Notation "< x y >" := (type_app x y) (at level 68, left associativity).
+Notation "'$' x" := (type_id x) (at level 66).
+*)
+
+End Terms.