Zulip Chat Archive

Stream: general

Topic: fail_if_success v success_if_fail


view this post on Zulip Kevin Buzzard (May 17 2020 at 15:58):

OK so what's the difference between fail_if_success and success_if_fail?

Source code is I think this:

meta def fail_if_success {α : Type u} (t : tactic α) : tactic unit :=
λ s, result.cases_on (t s)
 (λ a s, mk_exception "fail_if_success combinator failed, given tactic succeeded" none s)
 (λ e ref s', success () s)

meta def success_if_fail {α : Type u} (t : tactic α) : tactic unit :=
λ s, match t s with
| (interaction_monad.result.exception _ _ s') := success () s
| (interaction_monad.result.success a s) :=
   mk_exception "success_if_fail combinator failed, given tactic succeeded" none s
end

view this post on Zulip Mario Carneiro (May 17 2020 at 17:45):

these are identical. Not the best naming convention

view this post on Zulip Pedro Minicz (May 18 2020 at 16:10):

I believe the Coq naming convention would suit best in this case. In Coq you just have Fail some_command. Note, however, that this is different from the fail tactic, which is a tactic that always fail. Does Lean also have such tactic?

view this post on Zulip Pedro Minicz (May 18 2020 at 16:11):

Overloading this name shouldn't cause any confusion tho, fail some_tactic could behave like fail_if_success some_tactic and just fail could always fail if such tactic is deemed necessary.

view this post on Zulip Reid Barton (May 18 2020 at 16:17):

Is Fail a top-level command then?

view this post on Zulip Pedro Minicz (May 18 2020 at 16:23):

Yes, Fail is a vernacular command and fail is a tactic.

view this post on Zulip Pedro Minicz (May 18 2020 at 16:24):

Trivial question: does Lean also have this distinction? It appears to be the case with say tactics vs #-commands.

view this post on Zulip Simon Hudon (May 18 2020 at 16:26):

It does. Commands are created with the @[user_command]attribute and have to have the type parser unit while tactics have type tactic unit and have to be located in the interactive namespace for the parser to pick them up

view this post on Zulip Reid Barton (May 18 2020 at 16:28):

Do user commands force the preceding declaration to end (like lemma does for example)?

view this post on Zulip Simon Hudon (May 18 2020 at 16:31):

Mostly, yes. I think there is an issue with putting one right after the import section though (unless @Gabriel Ebner fixed it in the recent releases)

view this post on Zulip Gabriel Ebner (May 18 2020 at 16:32):

It was fixed a few releases ago. Just write the command in the first column and you're fine.

view this post on Zulip Reid Barton (May 18 2020 at 16:34):

So, effectively they do not live in a separate namespace


Last updated: May 11 2021 at 13:22 UTC