## Stream: general

### Topic: slim_check

#### Scott Morrison (Oct 07 2020 at 23:23):

An example just came up on another thread where some missing parentheses garbled a statement. I was hoping to be able to run slim_check on it, but couldn't.

import tactic.slim_check

example (f g : ℕ → Prop) : ∃ k : ℕ, f k ∨ ∃ k : ℕ, g k ↔ ∃ k : ℕ, f k ∨ g k :=
by slim_check


#### Scott Morrison (Oct 07 2020 at 23:24):

First, a little bug report: when this fails, it suggests running

set_option trace.class_instances true
#check (by apply_instance : testable (slim_check.named_binder "f"
(∀ (f : ℕ → Prop),
slim_check.named_binder "g"
(∀ (g : ℕ → Prop), ∃ (k : ℕ), f k ∨ ∃ (k : ℕ), g k ↔ ∃ (k : ℕ), f k ∨ g k))))


to see which instances are missing, but we get unknown identifier testable.

#### Scott Morrison (Oct 07 2020 at 23:25):

I can see that with the recent PR about sampleable, we at least get off the ground here:

#sample ℕ → Prop


produces lots of good candidate functions.

#### Simon Hudon (Oct 07 2020 at 23:25):

That's true, you need open slim_check. Sorry

#### Simon Hudon (Oct 07 2020 at 23:26):

An existential is difficult to test because there's no witness that shows that it's false

ah, of course!

#### Scott Morrison (Oct 07 2020 at 23:27):

How about we just replace testable with slim_check.testable in the suggestion text?

#### Simon Hudon (Oct 07 2020 at 23:27):

If it ranged over fin n even if you quantify over all n that should be better

#### Simon Hudon (Oct 07 2020 at 23:28):

I think that's a good idea

#### Scott Morrison (Oct 07 2020 at 23:28):

Your todo list or mine? :-)

#### Simon Hudon (Oct 07 2020 at 23:30):

How about whoever gets there first?

#### Bryan Gin-ge Chen (Oct 08 2020 at 03:44):

Simon won the race: #4520 (now on the queue)

#### Simon Hudon (Oct 08 2020 at 04:02):

That was one swift review!

Last updated: May 06 2021 at 22:13 UTC