From c3d1649402751151e435f58312736cc8528194ab Mon Sep 17 00:00:00 2001 From: Michael Sippel Date: Sun, 8 Sep 2024 14:48:36 +0200 Subject: [PATCH] expr term: remove explicit variable-type from expr_let --- coq/bbencode.v | 9 ++------- coq/subst.v | 2 +- coq/terms.v | 3 +-- 3 files changed, 4 insertions(+), 10 deletions(-) diff --git a/coq/bbencode.v b/coq/bbencode.v index 934d619..b795d31 100644 --- a/coq/bbencode.v +++ b/coq/bbencode.v @@ -55,13 +55,8 @@ Definition bb_succ : expr_term := (expr_var "z")))))))). Definition e1 : expr_term := - (expr_let "bb-zero" (type_ladder (type_id "ℕ") - (type_ladder (type_id "BBNat") - (type_univ "α" - (type_fun (type_fun (type_var "α") (type_var "α")) - (type_fun (type_var "α") (type_var "α")))))) - bb_zero - (expr_app (expr_app (expr_var "+") (expr_var "bb-zero")) (expr_var "bb-zero")) + (expr_let "bb-zero" bb_zero + (expr_app (expr_app (expr_var "+") (expr_var "bb-zero")) (expr_var "bb-zero")) ). Definition t1 : expr_term := (expr_app (expr_var "x") (expr_var "x")). diff --git a/coq/subst.v b/coq/subst.v index 3ad385d..02eb711 100644 --- a/coq/subst.v +++ b/coq/subst.v @@ -115,7 +115,7 @@ Fixpoint expr_subst (v:string) (n:expr_term) (e0:expr_term) := | expr_abs x t e => if (eqb v x) then e0 else expr_abs x t (expr_subst v n e) | expr_morph x t e => if (eqb v x) then e0 else expr_morph x t (expr_subst v n e) | expr_app e a => expr_app (expr_subst v n e) (expr_subst v n a) - | expr_let x t a e => expr_let x t (expr_subst v n a) (expr_subst v n e) + | expr_let x a e => expr_let x (expr_subst v n a) (expr_subst v n e) | expr_ascend t e => expr_ascend t (expr_subst v n e) | expr_descend t e => expr_descend t (expr_subst v n e) end. diff --git a/coq/terms.v b/coq/terms.v index 6201478..3cc59aa 100644 --- a/coq/terms.v +++ b/coq/terms.v @@ -25,12 +25,11 @@ Inductive expr_term : Type := | expr_abs : string -> type_term -> expr_term -> expr_term | expr_morph : string -> type_term -> expr_term -> expr_term | expr_app : expr_term -> expr_term -> expr_term - | expr_let : string -> type_term -> expr_term -> expr_term -> expr_term + | expr_let : string -> expr_term -> expr_term -> expr_term | expr_ascend : type_term -> expr_term -> expr_term | expr_descend : type_term -> expr_term -> expr_term . - (* TODO Inductive type_DeBruijn : Type :=