From 61948c6dc6a7e57188f4c05134d8f23cc7b10cf9 Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Wed, 24 Jul 2024 11:17:45 +0200
Subject: [PATCH] setup coq project & initial definition of terms (types &
 expressions)

---
 .gitignore      |  6 ++++++
 coq/_CoqProject |  8 ++++++++
 coq/terms.v     | 44 ++++++++++++++++++++++++++++++++++++++++++++
 3 files changed, 58 insertions(+)
 create mode 100644 .gitignore
 create mode 100644 coq/_CoqProject
 create mode 100644 coq/terms.v

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.