add(SecondOrder): Kind, Typ and Term definitions

keilambda · Nov 10, 2024 · 6cbf65f · 6cbf65f
1 parent 3e8748c
commit 6cbf65f
Showing 1 changed file with 24 additions and 0 deletions.
diff --git a/TTFPI/SecondOrder.lean b/TTFPI/SecondOrder.lean
@@ -1,2 +1,26 @@
+import TTFPI.Basic
+
 namespace SecondOrder
+
+inductive Kind where
+| star
+deriving Repr, DecidableEq
+
+notation " ∗ " => Kind.star
+
+inductive Typ where
+| var (name : Name)
+| arrow (dom : Typ) (codom : Typ)
+| pi (param : Name) (kind : Kind) (body : Typ)
+deriving Repr, DecidableEq
+
+-- 3.4.1: Second order pre-typed λ-terms
+inductive Term where
+| var (name : Name)
+| app (fn : Term) (arg : Term)
+| tapp (fn : Term) (arg : Typ)
+| abs (param : Name) (type : Typ) (body : Term)
+| tabs (param : Name) (kind : Kind) (body : Term)
+deriving Repr, DecidableEq
+
 end SecondOrder