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

feat(library/init/meta/tactic): make sure to_format ==> to_tactic_format has higher priority

Browse source
This commit is contained in:
Leonardo de Moura 2016-06-27 14:34:55 +01:00
parent afffd31a7b
commit 669f8fc9df
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -31,9 +31,6 @@ do s ← tactic.read, return (tactic_state.format_expr s e)
structure has_to_tactic_format [class] (A : Type) :=
(to_tactic_format : A → tactic format)
meta_definition has_to_format_to_has_to_tactic_format [instance] (A : Type) [has_to_format A] : has_to_tactic_format A :=
has_to_tactic_format.mk (return ∘ to_fmt)
meta_definition expr_has_to_tactic_format [instance] : has_to_tactic_format expr :=
has_to_tactic_format.mk tactic.format_expr
@ -58,6 +55,9 @@ meta_definition list_to_tactic_format {A : Type} [has_to_tactic_format A] : list
meta_definition list_has_to_tactic_format [instance] {A : Type} [has_to_tactic_format A] : has_to_tactic_format (list A) :=
has_to_tactic_format.mk list_to_tactic_format
meta_definition has_to_format_to_has_to_tactic_format [instance] (A : Type) [has_to_format A] : has_to_tactic_format A :=
has_to_tactic_format.mk (return ∘ to_fmt)
namespace tactic
open tactic_state