From 26d9cb3da795010b3e4e2110e155e8b13ed2c2c0 Mon Sep 17 00:00:00 2001
From: PratherConid <syxx2013050321@163.com>
Date: Fri, 10 Jan 2025 20:29:48 -0800
Subject: [PATCH] set ignorenonquasi option

---
 Auto/EvaluateAuto/TestAuto.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/Auto/EvaluateAuto/TestAuto.lean b/Auto/EvaluateAuto/TestAuto.lean
index 3fc94d3..426f058 100644
--- 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",