Add meta theorems about disjunctions and conjunctions#59
Add meta theorems about disjunctions and conjunctions#59fblanqui merged 3 commits intoDeducteam:masterfrom
Conversation
fblanqui
left a comment
fblanqui
left a comment
There was a problem hiding this comment.
Thanks Melanie! That's nice! Just a few things to change.
|
Let me know when you implemented those changes. |
The changes you asked for were all implemented in my last commit! |
MetaTheorems.lp
Outdated
| // lemmas on ∈ₙ | ||
|
|
||
| opaque symbol indexes_shift (l: 𝕃 nat) (n : τ nat): | ||
| π (istrue ((n +1) ∈ₙ (map (+1) l)) ⇒ istrue (n ∈ₙ l))≔ |
There was a problem hiding this comment.
There are still some istrue's here and later as well. Could you please try to get rid of all of them, if possible?
CHANGES.md
Outdated
|
|
||
| ### Added | ||
|
|
||
| - MetaTheorems: theorems for structural operations on the level of clauses and literals |
There was a problem hiding this comment.
What about splitting this file in 2: Disj and Conj?
There was a problem hiding this comment.
Yes, good idea!
fblanqui
changed the title
|
In the new commit, I removed all instances of "istrue" in my theorems, and I tried to remve all superfluous parentheses from the theorems. As you @fblanqui suggested, I split MetaTheorems into two file and as a result moved shared lemmas to list.lp. |
|
Thank you Melanie! @NotBad4U @ciaran-matthew-dunne @bodeveix @AntineaOgg |
2 participants
Add: