set ignorenonquasi option

leanprover-community · Jan 11, 2025 · 26d9cb3 · 26d9cb3
1 parent 128b097
commit 26d9cb3
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/Auto/EvaluateAuto/TestAuto.lean b/Auto/EvaluateAuto/TestAuto.lean
@@ -265,6 +265,8 @@ where
       ] ++ thmsStrs ++ [
         "]",
         "",
+        "set_option auto.mono.ignoreNonQuasiHigherOrder true",
+        "",
         "def action : CoreM Unit := do",
         "  let p ← initSrcSearchPath",
         s!"  let _ ← runAutoOnConsts",