fail_if_success v success_if_fail

Stream: general

[Kevin Buzzard]

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

[Mario Carneiro]

these are identical. Not the best naming convention

[Pedro Minicz]

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?

[Pedro Minicz]

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.

[Reid Barton]

Is Fail a top-level command then?

[Pedro Minicz]

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

[Pedro Minicz]

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

[Simon Hudon]

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

[Reid Barton]

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

[Simon Hudon]

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)

[Gabriel Ebner]

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

[Reid Barton]

So, effectively they do not live in a separate namespace