Commit 2387337b authored by Raphael Cauderlier's avatar Raphael Cauderlier

[resolution] Fix a bug caused by a partial function application that

did not reduce
parent 37551216
......@@ -136,10 +136,10 @@ def magic_imp : l : clauses.litteral -> l' : clauses.litteral -> lproof l -> lpr
(; /!\ magic_or_imp l C H only reduces if l ∈ C ;)
def magic_or_imp : l : clauses.litteral -> C : clauses.clause -> lproof l -> cproof C.
[l,C,H] magic_or_imp l (clauses.cons_clause l C) H -->
or_intro_1 (lprop l) (cprop C) H
[l1,l2,C,H] magic_or_imp l1 (clauses.cons_clause l2 C) H -->
or_intro_2 (lprop l2) (cprop C) (magic_or_imp l1 C H).
[l,C] magic_or_imp l (clauses.cons_clause l C) -->
or_intro_1 (lprop l) (cprop C)
[l1,l2,C] magic_or_imp l1 (clauses.cons_clause l2 C) -->
H => or_intro_2 (lprop l2) (cprop C) (magic_or_imp l1 C H).
(; /!\ magic_remove l C H only reduces if l ∈ C ;)
def magic_remove (l : clauses.litteral) (C : clauses.clause) (H : cproof (clauses.cons_clause l C)) : cproof C :=
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment