From f8331a0dfeec08fd8ed298f0bf64567585471df4 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Tue, 27 Dec 2016 16:58:53 +0100 Subject: [PATCH] fix(library/tools/super/prover_state): correctly detect sos lemmas --- library/tools/super/prover_state.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/tools/super/prover_state.lean b/library/tools/super/prover_state.lean index 29c65eeea1..855ddbb1c5 100644 --- a/library/tools/super/prover_state.lean +++ b/library/tools/super/prover_state.lean @@ -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,