chore: add module keyword to grind tests

This PR also fixes missing `@[expose]` in grind support definitions.

src/Init/Data/Ord/Basic.lean

@@ -96,7 +96,7 @@ Ordering.lt
   | a => a
 
 /-- Version of `Ordering.then'` for proof by reflection. -/
-noncomputable def then' (a b : Ordering) : Ordering :=
+@[expose] noncomputable def then' (a b : Ordering) : Ordering :=
   Ordering.rec a b a a
 
 /--

src/Init/Grind/Ordered/Linarith.lean

@@ -12,7 +12,7 @@ public import all Init.Data.Ord.Basic
 public import all Init.Data.AC
 public import Init.Data.RArray
 
-public section
+@[expose] public section
 
 /-!
 Support for the linear arithmetic module for `IntModule` in `grind`

src/Init/Grind/ToInt.lean

@@ -46,9 +46,9 @@ instance : LawfulBEq IntInterval where
 namespace IntInterval
 
 /-- The interval `[0, 2^n)`. -/
-abbrev uint (n : Nat) := IntInterval.co 0 (2 ^ n)
+@[expose] abbrev uint (n : Nat) := IntInterval.co 0 (2 ^ n)
 /-- The interval `[-2^(n-1), 2^(n-1))`. -/
-abbrev sint (n : Nat) := IntInterval.co (-(2 ^ (n - 1))) (2 ^ (n - 1))
+@[expose] abbrev sint (n : Nat) := IntInterval.co (-(2 ^ (n - 1))) (2 ^ (n - 1))
 
 /-- The lower bound of the interval, if finite. -/
 @[expose] def lo? (i : IntInterval) : Option Int :=
@@ -98,7 +98,7 @@ instance : Membership Int IntInterval where
 theorem nonEmpty_of_mem {x : Int} {i : IntInterval} (h : x ∈ i) : i.nonEmpty := by
   cases i <;> simp_all <;> omega
 
-@[simp]
+@[simp, expose]
 def wrap (i : IntInterval) (x : Int) : Int :=
   match i with
   | co lo hi => (x - lo) % (hi - lo) + lo

src/Lean/Meta/Tactic/Grind/Arith/CommRing/Poly.lean

@@ -31,11 +31,13 @@ def Mon.lcm : Mon → Mon → Mon
     | .lt => .mult pw₁ (lcm m₁ (.mult pw₂ m₂))
     | .gt => .mult pw₂ (lcm (.mult pw₁ m₁) m₂)
 
+-- Remark: we expose `Mon.divides` and `Mon.div` because we use then to write tests using `rfl`
+
 /--
 `divides m₁ m₂` returns `true` if monomial `m₁` divides `m₂`
 Example: `x^2.z` divides `w.x^3.y^2.z`
 -/
-def Mon.divides : Mon → Mon → Bool
+@[expose] def Mon.divides : Mon → Mon → Bool
   | .unit, _ => true
   | _, .unit => false
   | .mult pw₁ m₁, .mult pw₂ m₂ =>
@@ -49,7 +51,7 @@ Given `m₁` and `m₂` such that `m₂.divides m₁`, then
 `m₁.div m₂` returns the result.
 Example `w.x^3.y^2.z` div `x^2.z` returns `w.x.y^2`
 -/
-def Mon.div : Mon → Mon → Mon
+@[expose] def Mon.div : Mon → Mon → Mon
   | m₁, .unit => m₁
   | .unit, _  => .unit -- reachable only if pre-condition does not hold
   | .mult pw₁ m₁, .mult pw₂ m₂ =>

src/Std.lean

@@ -3,6 +3,7 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sebastian Ullrich
 -/
+module
 prelude
 import Std.Data
 import Std.Do

tests/lean/run/grind_9216.lean

@@ -1,3 +1,4 @@
+module
 import Std.Data.HashSet
 
 open Std

tests/lean/run/grind_9321.lean

@@ -1,3 +1,4 @@
+module
 example (z : Int) : z + (Int.cast (R := Int) (-2)) = z - 2 := by grind
 
 attribute [local instance] Lean.Grind.Semiring.natCast Lean.Grind.Ring.intCast

tests/lean/run/grind_9427.lean

@@ -1,3 +1,4 @@
+module
 example {n} (x y : BitVec n) : x * y = y * x := by
   grind
 

tests/lean/run/grind_9467.lean

@@ -1,3 +1,4 @@
+module
 example (x y : Nat) : (x : Int) - (y : Int) = 0 → x = y := by
   grind
 

tests/lean/run/grind_9477.lean

@@ -1,3 +1,4 @@
+module
 structure T where
   upper_bound : Nat
 

tests/lean/run/grind_9485.lean

@@ -1,3 +1,4 @@
+module
 variable (G : Type)
 
 structure G' where p : G

tests/lean/run/grind_9562.lean

@@ -1,3 +1,4 @@
+module
 axiom A : Type
 axiom angle (x y z : A) : Int
 axiom pi : Int

tests/lean/run/grind_9572.lean

@@ -1,3 +1,4 @@
+module
 def List.Disjoint (l₁ l₂ : List α) : Prop :=
   ∀ ⦃a⦄, a ∈ l₁ → a ∈ l₂ → False
 
@@ -11,7 +12,7 @@ l : List Nat
 h :
   ¬List.Pairwise
       (fun x y =>
-        (if x ^ i ≤ n then List.map (fun m => x :: m) (f x) else []).Disjoint
+        List.Disjoint (if x ^ i ≤ n then List.map (fun m => x :: m) (f x) else [])
           (if y ^ i ≤ n then List.map (fun m => y :: m) (f y) else []))
       l
 ⊢ False
@@ -19,13 +20,13 @@ h :
   [facts] Asserted facts
     [prop] ¬List.Pairwise
             (fun x y =>
-              (if x ^ i ≤ n then List.map (fun m => x :: m) (f x) else []).Disjoint
+              List.Disjoint (if x ^ i ≤ n then List.map (fun m => x :: m) (f x) else [])
                 (if y ^ i ≤ n then List.map (fun m => y :: m) (f y) else []))
             l
   [eqc] False propositions
     [prop] List.Pairwise
           (fun x y =>
-            (if x ^ i ≤ n then List.map (fun m => x :: m) (f x) else []).Disjoint
+            List.Disjoint (if x ^ i ≤ n then List.map (fun m => x :: m) (f x) else [])
               (if y ^ i ≤ n then List.map (fun m => y :: m) (f y) else []))
           l
 -/

tests/lean/run/grind_9610.lean

@@ -1,3 +1,4 @@
+module
 set_option warn.sorry false
 abbrev sixteen : UInt32 := 16
 

tests/lean/run/grind_9769.lean

@@ -1,3 +1,4 @@
+module
 def Foo (n : Nat) := Σ (m : Nat), {f : Fin (n + 2) → Fin (m + 2) // f 0 = 0}
 
 variable (n : Nat)

tests/lean/run/grind_9825.lean

@@ -1,3 +1,4 @@
+module
 import Lean.Elab.Command
 
 theorem extracted_1_1 {K : Type} [Lean.Grind.Field K] (pB ppB pBf ifpnf : K) :

tests/lean/run/grind_9828.lean

@@ -1,3 +1,4 @@
+module
 def Xor' (a b : Prop) := (a ∧ ¬b) ∨ (b ∧ ¬a)
 
 @[grind =] theorem xor_def {a b : Prop} : Xor' a b ↔ (a ∧ ¬b) ∨ (b ∧ ¬a) := Iff.rfl

tests/lean/run/grind_9830.lean

@@ -1,3 +1,4 @@
+module
 abbrev F : Fin 3 → Nat
 | 0 => 0
 | 1 => 1

tests/lean/run/grind_9854.lean

@@ -1,2 +1,3 @@
+module
 example (x: Nat) : UInt32.size - x < UInt64.size := by
   grind only

tests/lean/run/grind_9856.lean

@@ -1,3 +1,4 @@
+module
 inductive T (a:Type) where
   | constuctor1: T a
   | constuctor2: T a

tests/lean/run/grind_9897.lean

@@ -1,3 +1,4 @@
+module
 def Set' (α : Type u) := α → Prop
 
 namespace Set'

tests/lean/run/grind_9899.lean

@@ -1,3 +1,4 @@
+module
 namespace List
 -- Should not panic
 #guard_msgs (drop error) in

tests/lean/run/grind_9907.lean

@@ -1,3 +1,4 @@
+module
 structure DepThing {α : Type u} (l : List α) : Type u where
   suffix : List α
   property : suffix = l

tests/lean/run/grind_9948.lean

@@ -1,3 +1,4 @@
+module
 theorem sum_of_n (n : Nat) :
   (List.range (n + 1)).sum = n * (n + 1) / 2 := by
   induction n with

tests/lean/run/grind_Poly_mul_0_bug.lean

@@ -1,3 +1,4 @@
+module
 open Int.Linear
 
 def p : Poly := .add 1 1 <| .add 2 0 <| .num 3

tests/lean/run/grind_abstract_mvars.lean

@@ -1,3 +1,4 @@
+module
 example (xs : Array Nat)
     (w : ∀ (j : Nat), 0 ≤ j → ∀ (x : j < xs.size / 2), xs[j] = xs[xs.size - 1 - j])
     (i : Nat) (hi₁ : i < xs.reverse.size) (hi₂ : i < xs.size) (h : i < xs.size / 2) : xs.reverse[i] = xs[i] := by

tests/lean/run/grind_activate_local_issue.lean

@@ -1,3 +1,4 @@
+module
 opaque p : Nat → Prop
 
 -- Local forall should be activated only once

tests/lean/run/grind_all_singleton_patterns.lean

@@ -1,3 +1,4 @@
+module
 example (p : Nat → Prop) (h₁ : x < n) (h₂ : ¬ p x) : ∃ i, i < n ∧ ¬ p i := by
   grind
 

tests/lean/run/grind_append_issue.lean

@@ -1,3 +1,4 @@
+module
 reset_grind_attrs%
 attribute [grind] List.length_cons List.length_nil List.length_append
 attribute [grind] List.nil_append List.getElem_cons

tests/lean/run/grind_arith_nonstd_insts.lean

@@ -1,3 +1,4 @@
+module
 class Distrib (R : Type _) extends Mul R where
 
 namespace Nat

tests/lean/run/grind_array.lean

@@ -1,2 +1,3 @@
+module
 example {l : List α} {i : USize} {a : α} {h : i.toNat < l.toArray.size} :
     l.toArray.uset i a h = (l.set i.toNat a).toArray := by grind

tests/lean/run/grind_assoc.lean

@@ -1,3 +1,4 @@
+module
 def α : Type := sorry
 instance : Mul α := sorry
 

tests/lean/run/grind_attrs.lean

@@ -1,3 +1,4 @@
+module
 opaque R : Nat → Nat → Prop
 
 @[grind ->]

tests/lean/run/grind_beta.lean

@@ -1,3 +1,4 @@
+module
 def f (x : Nat) : Nat → Nat → Nat :=
   match x with
   | 0 => fun _ _ => 0

tests/lean/run/grind_big_poly.lean

@@ -1,3 +1,4 @@
+module
 /--
 trace: [grind.issues] maximum recursion depth has been reached
     use `set_option maxRecDepth <num>` to increase limit

tests/lean/run/grind_bigstep.lean

@@ -1,3 +1,5 @@
+module
+@[expose] public section
 abbrev Variable := String
 
 def State := Variable → Nat

tests/lean/run/grind_bintree.lean

@@ -1,5 +1,6 @@
+module
 reset_grind_attrs%
-
+public section -- TODO: workaround for private declaration + dot-notation issue
 attribute [grind] List.append_assoc List.cons_append List.nil_append
 
 inductive Tree (β : Type v) where

tests/lean/run/grind_bitvec.lean

@@ -1,3 +1,4 @@
+module
 open BitVec
 
 example (x : BitVec (w+1)) : (cons x.msb (x.setWidth w)) = x := by

tests/lean/run/grind_bitvec2.lean

@@ -1,3 +1,4 @@
+module
 set_option linter.unusedSimpArgs false
 
 open BitVec

tests/lean/run/grind_bool_diseq.lean

@@ -1,3 +1,4 @@
+module
 example (f : Bool → Nat) : (x = y ↔ q) → ¬ q → y = false → f x = 0 → f true = 0 := by
   grind (splits := 0)
 

tests/lean/run/grind_bool_prop.lean

@@ -1,3 +1,4 @@
+module
 example (f : Bool → Nat) : f (a && b) = 0 → a = false → f false = 0 := by grind (splits := 0)
 example (f : Bool → Nat) : f (a && b) = 0 → b = false → f false = 0 := by grind (splits := 0)
 example (f : Bool → Nat) : f (a && b) = 0 → a = true → f b = 0 := by grind (splits := 0)

tests/lean/run/grind_canon_bug.lean

@@ -1,3 +1,4 @@
+module
 open List
 
 attribute [grind =] getElem_cons_zero

tests/lean/run/grind_canon_insts.lean

@@ -1,5 +1,6 @@
-import Lean.Meta.Tactic.Grind
-
+module
+public import Lean.Meta.Tactic.Grind
+public section
 set_option grind.debug true
 
 class Semigroup (α : Type u) extends Mul α where

tests/lean/run/grind_canon_types.lean

@@ -1,3 +1,4 @@
+module
 import Lean.Meta.Tactic.Grind
 
 def g (s : Type) := s

tests/lean/run/grind_cases.lean

@@ -1,3 +1,4 @@
+module
 /--
 error: invalid `[grind cases eager]`, `List` is not a non-recursive inductive datatype or an alias for one
 -/

tests/lean/run/grind_cases_tac.lean

@@ -1,4 +1,6 @@
-import Lean
+module
+public import Lean
+public meta import Lean.Elab.Tactic
 
 open Lean Meta Grind Elab Tactic in
 elab "cases' " e:term : tactic => withMainContext do

tests/lean/run/grind_casting_issue.lean

@@ -1,3 +1,4 @@
+module
 
 @[grind] def codelen (c: List Bool) : Int := c.length
 

tests/lean/run/grind_cat.lean

@@ -1,3 +1,5 @@
+module
+@[expose] public section
 universe v v₁ v₂ v₃ u u₁ u₂ u₃
 
 namespace CategoryTheory

tests/lean/run/grind_cat2.lean

@@ -1,3 +1,5 @@
+module
+@[expose] public section
 -- import Lean.Meta.Tactic.Grind
 universe v v₁ v₂ v₃ u u₁ u₂ u₃
 

tests/lean/run/grind_clear_error.lean

@@ -1,3 +1,4 @@
+module
 reset_grind_attrs%
 attribute [grind] List.not_mem_nil
 

tests/lean/run/grind_congr.lean

@@ -1,3 +1,4 @@
+module
 import Lean
 def f (a : Nat) := a + a + a
 def g (a : Nat) := a + a

tests/lean/run/grind_congr1.lean

@@ -1,3 +1,4 @@
+module
 set_option warningAsError false
 set_option grind.debug true
 set_option grind.debug.proofs true

tests/lean/run/grind_congr_hash_issue.lean

@@ -1,3 +1,4 @@
+module
 set_option grind.debug true
 
 opaque f : Nat → Nat

tests/lean/run/grind_congr_over_applied.lean

@@ -1,3 +1,4 @@
+module
 example {g : (Int → Bool) → Int → Bool} {f : Int → Bool} {a b : Int} (hab : a = b) :
     Nat.repeat g 1 f a = Nat.repeat g 1 f b := by
   grind

tests/lean/run/grind_constProp.lean

@@ -1,4 +1,6 @@
+module
 reset_grind_attrs%
+@[expose] public section -- TODO: remove after we fix congr_eq
 
 attribute [grind cases] Or
 attribute [grind =] List.length_nil List.length_cons Option.getD

tests/lean/run/grind_const_pattern.lean

@@ -1,3 +1,4 @@
+module
 reset_grind_attrs%
 
 attribute [grind] List.map_append

tests/lean/run/grind_countP.lean

@@ -1,3 +1,4 @@
+module
 variable {α : Type u} {l : List α} {P Q : α → Bool}
 
 attribute [grind] List.countP_nil List.countP_cons

tests/lean/run/grind_ctor_ematch.lean

@@ -1,3 +1,4 @@
+module
 inductive Even : Nat → Prop
   | zero : Even 0
   | plus_two {n} : Even n → Even (n + 2)

tests/lean/run/grind_cutsat_auto.lean

@@ -1,3 +1,4 @@
+module
 example : ∀ x : Int, x > 7 → 2 * x > 14 := by
   grind
 

tests/lean/run/grind_cutsat_commring.lean

@@ -1,3 +1,4 @@
+module
 open Lean.Grind
 
 variable [CommRing R] [LE R] [LT R] [LinearOrder R] [OrderedRing R]

tests/lean/run/grind_cutsat_cooper.lean

@@ -1,3 +1,4 @@
+module
 
 example (x y : Int) :
     27 ≤ 11*x + 13*y →

tests/lean/run/grind_cutsat_decompose.lean

@@ -1,2 +1,3 @@
+module
 example (n : Int) : n = 1000 * (n / 1000) + 100 * ((n / 100) % 10) + 10 * ((n / 10) % 10) + n % 10 := by
   grind

tests/lean/run/grind_cutsat_diseq_1.lean

@@ -1,3 +1,4 @@
+module
 set_option grind.debug true
 open Int.Linear
 

tests/lean/run/grind_cutsat_diseq_2.lean

@@ -1,3 +1,4 @@
+module
 set_option grind.debug true
 open Int.Linear
 

tests/lean/run/grind_cutsat_diseq_3.lean

@@ -1,3 +1,4 @@
+module
 set_option grind.debug true
 open Int.Linear
 

tests/lean/run/grind_cutsat_diseq_cooper.lean

@@ -1,3 +1,4 @@
+module
 theorem ex1 (x : Int) : 10 ≤ x → x ≤ 20 → x ≠ 11 → 11 ∣ x → False := by
   grind
 

tests/lean/run/grind_cutsat_div_1.lean

@@ -1,3 +1,4 @@
+module
 set_option grind.debug true
 set_option pp.structureInstances false
 open Int.Linear

tests/lean/run/grind_cutsat_div_mod.lean

@@ -1,3 +1,4 @@
+module
 example (x y : Int) : x / 2 + y = 3 → x = 5 → y = 1 := by
   grind
 

tests/lean/run/grind_cutsat_eq_1.lean

@@ -1,3 +1,4 @@
+module
 set_option grind.debug true
 open Int.Linear
 

tests/lean/run/grind_cutsat_instances.lean

@@ -1,3 +1,4 @@
+module
 class Distrib (R : Type _) extends Mul R where
 
 namespace Nat

tests/lean/run/grind_cutsat_le_1.lean

@@ -1,3 +1,4 @@
+module
 set_option grind.debug true
 
 /--

tests/lean/run/grind_cutsat_le_2.lean

@@ -1,3 +1,4 @@
+module
 set_option grind.debug true
 open Int.Linear
 

tests/lean/run/grind_cutsat_natCast_propagation.lean

@@ -1,3 +1,4 @@
+module
 example (a b : Nat) : a  = a + b - b := by
   grind
 

tests/lean/run/grind_cutsat_nat_dvd.lean

@@ -1,3 +1,4 @@
+module
 theorem ex₁ (a : Nat) (h₁ : 2 ∣ a) (h₂ : 2 ∣ a + 1) : False := by
   grind
 

tests/lean/run/grind_cutsat_nat_eq.lean

@@ -1,3 +1,4 @@
+module
 example (a b c : Nat) : a = 0 → b = 0 → c ≥ a + b := by
   grind
 

tests/lean/run/grind_cutsat_nat_le.lean

@@ -1,3 +1,4 @@
+module
 
 open Int.Linear
 

tests/lean/run/grind_cutsat_omega.lean

@@ -1,3 +1,4 @@
+module
 example (_ : (1 : Int) < (0 : Int)) : False := by grind
 example (_ : (0 : Int) < (0 : Int)) : False := by grind
 example (_ : (0 : Int) < (1 : Int)) : True := by grind

tests/lean/run/grind_cutsat_tests.lean

@@ -1,3 +1,4 @@
+module
 example (w x y z : Int) :
   2*w + 3*x - 4*y + z = 10 →
   w - x + 2*y - 3*z = 5 →

tests/lean/run/grind_cutsat_toint_1.lean

@@ -1,3 +1,4 @@
+module
 example (a b c : Fin 11) : a ≤ b → b ≤ c → a ≤ c := by
   grind
 

tests/lean/run/grind_cutsat_trim_context.lean

@@ -1,3 +1,4 @@
+module
 /--
 trace: [grind.debug.proof] fun h h_1 h_2 h_3 h_4 h_5 h_6 h_7 h_8 =>
       let ctx := RArray.leaf (f 2);

tests/lean/run/grind_cutsat_upper_bug.lean

@@ -1,3 +1,4 @@
+module
 /-- trace: [grind.cutsat.model] a := 2 -/
 #guard_msgs (trace) in
 set_option trace.grind.cutsat.model true in

tests/lean/run/grind_cutsat_zero.lean

@@ -1 +1,2 @@
+module
 example (hy : y = 0) (hz : z = 0) : 0 = y + z := by grind

tests/lean/run/grind_decide_bool_issues.lean

@@ -1,3 +1,4 @@
+module
 reset_grind_attrs%
 
 example {P Q : Prop} [Decidable P] [Decidable Q] : (decide P || decide Q) = decide (P ∨ Q) := by grind

tests/lean/run/grind_dep_match_overlap.lean

@@ -1,7 +1,10 @@
+module
+@[expose] public section -- TODO: remove after we fix congr_eq
 inductive Vec (α : Type u) : Nat → Type u
   | nil : Vec α 0
   | cons : α → Vec α n → Vec α (n+1)
 
+-- The `grind` tactics fail without this `[expose]`
 def h (v w : Vec α n) : Nat :=
   match v, w with
   | _, .cons _ (.cons _ _) => 20

tests/lean/run/grind_diseq.lean

@@ -1,3 +1,4 @@
+module
 set_option grind.debug true
 
 example (p q : Prop) (a b c d : Nat) :

tests/lean/run/grind_diseq_api.lean

@@ -1,3 +1,4 @@
+module
 import Lean
 
 opaque a : Nat

tests/lean/run/grind_dvd_propagate_issue.lean

@@ -1,3 +1,4 @@
+module
 open List
 
 

tests/lean/run/grind_ematch1.lean

@@ -1,5 +1,6 @@
+module
 reset_grind_attrs%
-
+public section
 set_option trace.grind.ematch.pattern true
 
 attribute [grind =] Array.size_set

tests/lean/run/grind_ematch2.lean

@@ -1,3 +1,4 @@
+module
 reset_grind_attrs%
 
 attribute [grind =] Array.size_set Array.getElem_set_self Array.getElem_set_ne

tests/lean/run/grind_ematch_gen_pattern.lean

@@ -1,3 +1,4 @@
+module
 def f (x : Option Nat) (h : x ≠ none) : Nat :=
   match x with
   | none => by contradiction

tests/lean/run/grind_ematch_ground_implicit_inst.lean

@@ -1,3 +1,4 @@
+module
 example (a : Nat) : max a a = a := by
   grind
 

tests/lean/run/grind_ematch_patterns.lean

@@ -1,3 +1,5 @@
+module
+public section -- TODO: Fix error messages with private names.
 def replicate : (n : Nat) → (a : α) → List α
   | 0,   _ => []
   | n+1, a => a :: replicate n a

tests/lean/run/grind_ematch_theorem_activation.lean

@@ -1,3 +1,4 @@
+module
 reset_grind_attrs%
 attribute [grind] List.length_set
 attribute [grind →] List.eq_nil_of_length_eq_zero

tests/lean/run/grind_ematch_type_error.lean

@@ -1,3 +1,4 @@
+module
 example (xs : Array Nat) (w : xs.reverse = xs) (j : Nat) (hj : 0 ≤ j) (hj' : j < xs.size / 2) :
     xs[j] = xs[xs.size - 1 - j] := by
   grind

tests/lean/run/grind_eq.lean

@@ -1,3 +1,4 @@
+module
 opaque g : Nat → Nat
 
 set_option trace.Meta.debug true

tests/lean/run/grind_eq_bwd.lean

@@ -1,3 +1,4 @@
+module
 theorem dummy (x : Nat) : x = x :=
   rfl
 

tests/lean/run/grind_eq_bwd_pat_bug.lean

@@ -1,3 +1,4 @@
+module
 @[grind ←=] theorem inv_eq {α : Type} [One α] [Mul α] [Inv α] {a b : α} (w : a * b = 1) : a⁻¹ = b := sorry
 
 theorem test {α : Type} [One α] [Mul α] [Inv α] {a b : α} (w : a * b = 1) : a⁻¹ = b := by

tests/lean/run/grind_eq_false_of_imp_eq_false.lean

@@ -1,3 +1,4 @@
+module
 reset_grind_attrs%
 open List
 

tests/lean/run/grind_eq_pattern.lean

@@ -1,3 +1,4 @@
+module
 reset_grind_attrs%
 
 /--

tests/lean/run/grind_eqres_bug.lean

@@ -1,3 +1,4 @@
+module
 /--
 trace: [grind.eqResolution] ∀ (x : Nat), p x a → ∀ (y : Nat), p y b → ¬x = y, ∀ (y : Nat), p y a → p y b → False
 [grind.ematch.instance] local_0: p c a → ¬p c b