`assumption?`

[jalex-stark]

See this topic and this topic on zulip.

[gebner]

I feel obligated to mention that you could also implement assumption? in mathlib using the trick described here.

[gebner]

bors try

[bors[bot]]

try

Build failed:

• Build linux Release

[gebner]

bors try

[bors[bot]]

try

Build failed:

• Build linux Release

[gebner]

I think for the ? notation to work, you need to add this before assumption: (copied from rcases)

precedence `?`:max

You should also add an assumption' tactic (of type tactic unit) that you can use as auto_param. That is, replace . assumption by . assumption' in two tests.

[jalex-stark]

I think for the ? notation to work, you need to add this before assumption: (copied from rcases)

precedence `?`:max

You should also add an assumption' tactic (of type tactic unit) that you can use as auto_param. That is, replace . assumption by . assumption' in two tests.

There's currently an assumption' tactic that's essentially all_goals {assumption}. which one deserves the name? (I don't know what an auto_param is, and I don't know which two tests you want replaced.)

[gebner]

If you write . assumption after the type of an argument, then Lean will try to automatically fill in the argument by calling the tactic assumption. This is also works for structure fields.

There are two tests that use . assumption (just search for it). The auto_param is definitely the least important, the current assumption' should stay as it is.

[jalex-stark]

If you write . assumption after the type of an argument, then Lean will try to automatically fill in the argument by calling the tactic assumption. This is also works for structure fields.

There are two tests that use . assumption (just search for it). The auto_param is definitely the least important, the current assumption' should stay as it is.

so these tests need . assumption replaced by . tactic.assumption? or we should make assumption'' an alias for tactic.assumption? (I don't really know what's going on and my instinct is to blindly try to implement what you tell me.)

[jalex-stark]

in the latest commit, I have ./test_single.sh ../../bin/lean assumption.lean gives output -- checked

but the . assumption tests are I think still broken, working on it.

[gebner]

I think you should add an assumption'' and use that in the tests.

bors try

[bors[bot]]

try

Build failed:

• Build linux Release

[gebner]

Oh wow, the precedence change broke a lot of stuff. You should post a message on Zulip about this. I'm not sure what the correct solution here is.

[jalex-stark]

I feel obligated to mention that you could also implement assumption? in mathlib using the trick described here.

Maybe this approach would get around the current problem. Note that rcases is in mathlib and the precedence stuff doesn't break there.