max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor(library/init/meta/base_tactic): merge fail and fail_fmt

Browse source
This commit is contained in:
Leonardo de Moura 2016-06-23 09:12:57 -07:00
parent 8b53e8000a
commit affd9d4557
1 changed files with 2 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
library/init/meta/base_tactic.lean
View file

@ -57,11 +57,8 @@ namespace tactic
variables {S A : Type}
open base_tactic_result
meta_definition fail (e : string) : base_tactic S A :=
λ s, exception A (λ u, to_fmt e) s
meta_definition fail_fmt (e : format) : base_tactic S A :=
λ s, exception A (λ u, e) s
meta_definition fail {A B : Type} [has_to_format B] (msg : B) : base_tactic S A :=
λ s, exception A (λ u, to_fmt msg) s
meta_definition failed : base_tactic S A :=
fail "failed"