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

fix(library/tools/super/prover_state): correctly detect sos lemmas

Browse source
This commit is contained in:
Gabriel Ebner 2016-12-27 16:58:53 +01:00 • committed by Leonardo de Moura
parent fb54126d08
commit f8331a0dfe
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/tools/super/prover_state.lean
View file

@ -406,7 +406,7 @@ meta def empty (local_false : expr) : prover_state :=
meta def initial (local_false : expr) (clauses : list clause) : tactic prover_state := do
after_setup ← for' clauses (λc,
let in_sos := decidable.to_bool ((contained_lconsts c^.proof)^.size = 0) in
let in_sos := decidable.to_bool $ ((contained_lconsts c^.proof)^.erase local_false^.local_uniq_name)^.size = 0 in
do mk_derived c { priority := score.prio.immediate, in_sos := in_sos,
age := 0, cost := 0 } >>= add_inferred
) $ empty local_false,