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

feat(library/init/meta/match_tactic): add tactic_format for pattern

Browse source
This commit is contained in:
Johannes Hölzl 2017-02-20 11:12:11 -05:00 • committed by Leonardo de Moura
parent 0ad5f5bc89
commit 69ed20f656
1 changed files with 9 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
library/init/meta/match_tactic.lean
View file

@ -103,4 +103,13 @@ do ctx ← local_context,
new_p ← pexpr_to_pattern p,
match_hypothesis_core new_p ctx
meta instance : has_to_tactic_format pattern :=
⟨λp, do
t ← pp p^.target,
mo ← pp p^.moutput,
uo ← pp p^.uoutput,
u ← pp p^.nuvars,
m ← pp p^.nmvars,
return $ to_fmt "pattern.mk (" ++ t ++ ") " ++ uo ++ " " ++ mo ++ " " ++ u ++ " " ++ m ++ "" ⟩
end tactic