Skip to content
Snippets Groups Projects
Commit f50efde1 authored by SimonGuilloud's avatar SimonGuilloud
Browse files

start to work on set theory thorems

parent 84468083
No related branches found
No related tags found
1 merge request!6Various corrections, new set theory development as better examples.
package proven.DSetTheory
import lisa.kernel.fol.FOL.*
import lisa.kernel.proof.SequentCalculus.*
import lisa.KernelHelpers.{*, given}
import lisa.kernel.Printer
import proven.tactics.ProofTactics.*
import proven.tactics.Destructors.*
import lisa.settheory.AxiomaticSetTheory.*
import scala.collection.immutable.SortedSet
import lisa.kernel.proof.{SCProof, SCProofChecker}
import scala.collection.immutable
object Part1 {
/**
*/
val noSetCOntainsItself: SCProof = {
val contra = (y in y) <=> !(y in y)
val s1 = Hypothesis(contra |- contra, contra)
val s2 = LeftForall
}
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment