From eba78e2d83a772e92d91573e1fc51578a4df75e4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 19 Nov 2020 19:10:49 -0800 Subject: [PATCH] test: renaming for intrinsically typed lambda calculus --- tests/lean/run/renaming.lean | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) create mode 100644 tests/lean/run/renaming.lean diff --git a/tests/lean/run/renaming.lean b/tests/lean/run/renaming.lean new file mode 100644 index 0000000000..4534517ed6 --- /dev/null +++ b/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)