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

feat(tools/super/inhabited): look in the local context as well

Browse source
This commit is contained in:
Gabriel Ebner 2017-01-12 10:36:53 +01:00
parent b5ac381a5e
commit 42eb3ef497
1 changed files with 9 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
library/tools/super/inhabited.lean
View file

@ -8,6 +8,11 @@ open expr tactic monad
namespace super
meta def try_assumption_lookup_left (c : clause) : tactic (list clause) :=
on_first_left c $ λtype, do
ass ← find_assumption type,
return [([], ass)]
meta def try_nonempty_lookup_left (c : clause) : tactic (list clause) :=
on_first_left_dn c $ λhnx,
match is_local_not c^.local_false hnx^.local_type with
@ -62,9 +67,10 @@ on_first_right' c $ λhinh,
@[super.inf]
meta def inhabited_infs : inf_decl := inf_decl.mk 10 $ take given, do
for' [try_nonempty_lookup_left,
try_nonempty_left, try_nonempty_right,
try_inhabited_left, try_inhabited_right] $ λr,
for' [try_assumption_lookup_left,
try_nonempty_lookup_left,
try_nonempty_left, try_nonempty_right,
try_inhabited_left, try_inhabited_right] $ λr,
simp_if_successful given (r given^.c)
end super