From 4fde2442f160745b70d5814cd28f58fa91a04f1d Mon Sep 17 00:00:00 2001 From: Michael Sippel Date: Sun, 22 Sep 2024 13:36:20 +0200 Subject: [PATCH] fix naming of rules in expr_lc --- coq/terms/debruijn.v | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/coq/terms/debruijn.v b/coq/terms/debruijn.v index 54a6cdb..1c78ef0 100644 --- a/coq/terms/debruijn.v +++ b/coq/terms/debruijn.v @@ -280,8 +280,12 @@ Inductive expr_lc : expr_DeBruijn -> Prop := (type_lc σ) -> (forall x, (x `notin` L) -> expr_lc (expr_open (ex_fvar x) e1)) -> expr_lc (ex_abs σ e1) - | Tlc_App : forall e1 e2, expr_lc e1 -> expr_lc e2 -> expr_lc (ex_app e1 e2) - | Tlc_Let : forall e1 e2, expr_lc e1 -> expr_lc e2 -> expr_lc (ex_let e1 e2) - | Tlc_Ascend : forall τ e, type_lc τ -> expr_lc e -> expr_lc (ex_ascend τ e) - | Tlc_Descend : forall τ e, type_lc τ -> expr_lc e -> expr_lc (ex_descend τ e) + | Elc_Morph : forall σ e1 L, + (type_lc σ) -> + (forall x, (x `notin` L) -> expr_lc (expr_open (ex_fvar x) e1)) -> + expr_lc (ex_morph σ e1) + | Elc_App : forall e1 e2, expr_lc e1 -> expr_lc e2 -> expr_lc (ex_app e1 e2) + | Elc_Let : forall e1 e2, expr_lc e1 -> expr_lc e2 -> expr_lc (ex_let e1 e2) + | Elc_Ascend : forall τ e, type_lc τ -> expr_lc e -> expr_lc (ex_ascend τ e) + | Elc_Descend : forall τ e, type_lc τ -> expr_lc e -> expr_lc (ex_descend τ e) .