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

feat(library/init/meta/tactic): add to_string instance

Browse source
This commit is contained in:
Leonardo de Moura 2017-02-25 12:47:46 -08:00
parent 5a924699d0
commit 35acad642c
1 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
library/init/meta/tactic.lean
View file

@ -27,6 +27,9 @@ end tactic_state
meta instance : has_to_format tactic_state :=
⟨tactic_state.to_format⟩
meta instance : has_to_string tactic_state :=
⟨λ s, (to_fmt s)^.to_string s^.get_options⟩
@[reducible] meta def tactic := interaction_monad tactic_state
@[reducible] meta def tactic_result := interaction_monad.result tactic_state