## Stream: general

### Topic: fail_if_success v success_if_fail

#### 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
mk_exception "success_if_fail combinator failed, given tactic succeeded" none s
end


#### Mario Carneiro (May 17 2020 at 17:45):

these are identical. Not the best naming convention

#### 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?

#### 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.

#### Reid Barton (May 18 2020 at 16:17):

Is Fail a top-level command then?

#### Pedro Minicz (May 18 2020 at 16:23):

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

#### 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.

#### 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

#### Reid Barton (May 18 2020 at 16:28):

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

#### 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)

#### 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.

#### 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