commit 61948c6dc6a7e57188f4c05134d8f23cc7b10cf9
Author: Michael Sippel <micha@fragmental.art>
Date:   Wed Jul 24 11:17:45 2024 +0200

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

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..4220aed
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,6 @@
+*.glob
+*.vo
+*.vok
+*.vos
+*.aux
+*.pdf
diff --git a/coq/_CoqProject b/coq/_CoqProject
new file mode 100644
index 0000000..bf9e0a6
--- /dev/null
+++ b/coq/_CoqProject
@@ -0,0 +1,8 @@
+-R . LadderTypes
+terms.v
+equiv.v
+subst.v
+typing.v
+smallstep.v
+bbencode.v
+
diff --git a/coq/terms.v b/coq/terms.v
new file mode 100644
index 0000000..484a462
--- /dev/null
+++ b/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.