test: renaming for intrinsically typed lambda calculus

tests/lean/run/renaming.lean

@@ -0,0 +1,28 @@
+-- Renaming for intrinsically typed lambda calculus
+
+inductive Ty
+  | base
+  | arr (a b : Ty)
+
+def Cxt := List Ty
+
+inductive Var : (g : Cxt) → (a : Ty) → Type
+  | vz {g a}   : Var (a :: g) a
+  | vs {g a b} : Var g a → Var (b :: g) a
+
+inductive Term : Cxt → Ty → Type
+  | var {g a}   : Var g a → Term g a
+  | app {g a b} : Term g (Ty.arr a b) → Term g a → Term g b
+  | abs {g a b} : Term (a :: g) b → Term g (Ty.arr a b)
+
+def Ren (g d : Cxt) :=
+  (a : Ty) → Var d a → Var g a
+
+def liftr {g d a} (r : Ren g d) : Ren (a :: g) (a :: d)
+  | _, Var.vz   => Var.vz
+  | _, Var.vs x => Var.vs (r _ x)
+
+def rename {g d : Cxt} : (r : Ren g d) → {a : Ty} → Term d a → Term g a
+  | r, _, Term.var x   => Term.var (r _ x)
+  | r, _, Term.app t u => Term.app (rename r t) (rename r u)
+  | r, _, Term.abs t   => Term.abs (rename (liftr r) t)