From 1acd0e560a52b6af67815feb1db583ccb62a1fc2 Mon Sep 17 00:00:00 2001 From: JOSHCLUNE Date: Thu, 17 Oct 2024 15:31:48 -0400 Subject: [PATCH] Propagate leadingForallQuasiMonomorphic bug fix --- Auto/Translation/Monomorphization.lean | 11 ----------- 1 file changed, 11 deletions(-) diff --git a/Auto/Translation/Monomorphization.lean b/Auto/Translation/Monomorphization.lean index 338d755..f935081 100644 --- a/Auto/Translation/Monomorphization.lean +++ b/Auto/Translation/Monomorphization.lean @@ -436,23 +436,12 @@ where return (← leadingForallQuasiMonomorphicAux fvars ty) && (← leadingForallQuasiMonomorphicAux (fvars.push xid) bodyi) else - /- - **TODO** Discuss the purpose of this code with Yicheng and determine whether it should - be included. Notably, including this code causes the following simple example to fail: - ``` - def even_int_fun (f : Int → Int) := ∀ x, f (-x) = f x - - example (f : Int → Int) (hf : ∀ x, f (-x) = f x) : even_int_fun f := by -- The goal is the same as hf - duper [hf, even_int_fun] {preprocessing := full} - ``` - let hol : Bool := match ty with | .forallE _ _ body _ => !body.hasLooseBVar 0 | _ => false if hol && (← getMode) == .fol then return false - -/ let fvarSet := HashSet.empty.insertMany fvars if ty.hasAnyFVar fvarSet.contains then return false