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

chore(tests/lean/run/display_hw_term_hack_deps): remove old test

Browse source
This commit is contained in:
Leonardo de Moura 2018-10-23 11:25:56 -07:00
parent 9d32aff0c6
commit f7f981285b
1 changed files with 0 additions and 24 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
tests/lean/run/display_hw_term_hack_deps.lean
View file

@ -1,24 +0,0 @@
import init.lean.parser.syntax
import init.lean.parser.parsec
import init.lean.ir.type_check init.lean.ir.ssa_check init.lean.ir.elim_phi init.lean.ir.parser
open tactic
meta def is_eqn_theorem : name → bool
| (name.mk_string (name.mk_string "equations" _) _) := tt
| _ := ff
#exit
meta def display_hw_term_hack_dependencies : tactic unit :=
do env ← get_env,
env.fold (return mk_name_set) $ λ d tac, do {
s ← tac,
if is_eqn_theorem d.to_name then return s
else d.value.mfold s $ λ e _ s, do
if !e.is_constant_of `wf_term_hack || s.contains d.to_name then return s
else trace d.to_name >> return (s.insert d.to_name) },
return ()
-- Uncomment following line to inspect all declarations that use wf_term_hack
-- #eval display_hw_term_hack_dependencies