internal grind error

Stream: lean4

[Bhavik Mehta]

Here's the example:

def List.Disjoint (l₁ l₂ : List α) : Prop :=
  ∀ ⦃a⦄, a ∈ l₁ → a ∈ l₂ → False

theorem test (f : Nat → List (List Nat)) {l : List Nat} :
    l.Pairwise
      (fun x y ↦
        (if x ^ i ≤ n then List.map (fun m ↦ x :: m) (f x) else []).Disjoint
        (if y ^ i ≤ n then List.map (fun m ↦ y :: m) (f y) else [])) := by
  grind

Is this a known problem, or should I make an issue for it?

[Bhavik Mehta]

Here's the error message:

internal `grind` error, term has not been internalized
  List.map (fun m => _fvar.2077 :: m) (@_fvar.557 _fvar.2077)

[Robin Arnez]

I think this is just a bug, so yeah make an issue for it on the Lean repo

[Bhavik Mehta]

lean4#9572