From b055d237ef64e76448a539a9143d9abda0bcf904 Mon Sep 17 00:00:00 2001 From: Davide Fissore Date: Mon, 6 May 2024 16:25:15 +0200 Subject: [PATCH] add tc.maybe-llam-tm in clean-term --- apps/tc/elpi/ho_compile.elpi | 1 + apps/tc/elpi/ho_link.elpi | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/apps/tc/elpi/ho_compile.elpi b/apps/tc/elpi/ho_compile.elpi index ade292964..feeb6c030 100644 --- a/apps/tc/elpi/ho_compile.elpi +++ b/apps/tc/elpi/ho_compile.elpi @@ -108,6 +108,7 @@ namespace tc { clean-term A B :- (pi t s r\ copy (tc.maybe-eta-tm t s) r :- !, copy t r) => (pi t s r\ copy (tc.maybe-beta-tm t s) r :- !, copy t r) => + (pi t s r\ copy (tc.maybe-llam-tm t s) r :- !, copy t r) => std.assert! (copy A B) "[TC] clean-term error". pred add-pi-problematic-terms diff --git a/apps/tc/elpi/ho_link.elpi b/apps/tc/elpi/ho_link.elpi index 45bef2f40..99cdc1e31 100644 --- a/apps/tc/elpi/ho_link.elpi +++ b/apps/tc/elpi/ho_link.elpi @@ -41,7 +41,7 @@ namespace tc { pred progress-eta-left i:term, o:term. progress-eta-left A _ :- var A, !, fail. - progress-eta-left (fun _ _ A) (fun _ _ B) :- var B, !, A = B. + progress-eta-left (fun _ _ A) (fun _ _ A). progress-eta-left A A' :- (name A; is-coq-term A), !, eta-expand A A'. pred progress-eta-right i:term, o:term.