From 2d557e51e49d5f4af0a14d47e71649bc895d3708 Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Wed, 4 Sep 2024 12:47:03 +0200
Subject: [PATCH] WIP coq: debruijn terms

---
 coq/terms.v | 28 +++++++++++++++++++++++++++-
 1 file changed, 27 insertions(+), 1 deletion(-)

diff --git a/coq/terms.v b/coq/terms.v
index ffa0fa3..6201478 100644
--- a/coq/terms.v
+++ b/coq/terms.v
@@ -30,6 +30,33 @@ Inductive expr_term : Type :=
   | expr_descend : type_term -> expr_term -> expr_term
 .
 
+
+(* TODO
+
+Inductive type_DeBruijn : Type :=
+  | id : nat -> type_DeBruijn
+  | var : nat -> type_DeBruijn
+  | fun : type_DeBruijn -> type_DeBruijn -> type_DeBruijn
+  | univ : type_DeBruijn -> type_DeBruijn
+  | spec : type_DeBruijn -> type_DeBruijn -> type_DeBruijn
+  | morph : type_DeBruijn -> type_DeBruijn -> type_DeBruijn
+  | ladder : type_DeBruijn -> type_DeBruijn -> type_DeBruijn
+
+Inductive expr_DeBruijn : Type :=
+  | var : nat -> expr_DeBruijn
+  | ty_abs : expr_DeBruijn -> expr_DeBruijn
+  | ty_app : expr_DeBruijn -> type_DeBruijn -> expr_Debruijn
+  | abs   : type_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
+  | morph : type_DeBruijn -> expr_DeBruijn -> expr_Debruijn
+  | app : expr_DeBruijn -> expr_DeBruijn -> expr_Debruijn
+  | let : type_DeBruijn -> expr_DeBruijn -> expr_Debruijn -> expr_Debruijn
+  | ascend : type_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
+  | descend : type_DeBruijn -> expr_DeBruijn -> expr_DeBruijn
+.
+*)
+
+
+
 (* values *)
 Inductive is_value : expr_term -> Prop :=
   | V_Abs : forall x τ e,
@@ -44,7 +71,6 @@ Inductive is_value : expr_term -> Prop :=
 .
 
 
-
 Declare Scope ladder_type_scope.
 Declare Scope ladder_expr_scope.
 Declare Custom Entry ladder_type.