Zulip Chat Archive

Stream: mathlib4

Topic: slim_check instantiating mvars missing?

Yakov Pechersky (Jul 11 2023 at 22:09):

import Mathlib.Tactic.SlimCheck
import Mathlib.Testing.SlimCheck.Gen
import Mathlib.Testing.SlimCheck.Sampleable
import Mathlib.Testing.SlimCheck.Testable

lemma foo (n : ℕ) : n = n := by
  cases n
  slim_check -- unknown free variable '_uniq.7'

Yakov Pechersky (Jul 11 2023 at 22:16):

Nope, it was the other one, withMainContext

Yakov Pechersky (Jul 11 2023 at 22:19):

#5823

Last updated: Dec 20 2023 at 11:08 UTC