Skip to content
  • SimonGuilloud's avatar
    70059505
    Atomics, improve lisa.fol.FOL's logic and simplify it (#194) · 70059505
    SimonGuilloud authored
    * Renamed some elements of the formula hierarchy using the word "atomic"
    
    * removed the match type for ***. Instead, use opaque types and extension methods. Should be a bit more efficient and less prone to dotty bugs
    
    * remove ***. Only ** left
    
    * removing apply for sequences (use applyUnsafe)
    
    * mostly good but one theorem doesn't pass anymore
    
    * everything goes, no more *** (i.e. no match type)
    
    * progress
    
    * PredKer
    
    * mend
    
    * ConstantAtomicLabel, AtomicFormula
    
    * All atomic renaming completed
    
    * back to compile
    
    * finished tests, removed ConsOrPred
    
    * next step: Removes contravariant labels and terms and formulas extending |->
    
    * finish predicates, compiles
    
    * progress, Binders to sort and organize, some renaming to do in other files. Can remove - in labels.
    
    * finished cleaning and uniformizing definitions in Commons.scala, adapted other files accordingly. Compiles, tests passes, formated.
    
    * re-checked some warning, removed some redundant type checks.
    
    * fix substituteUnsafe2
    
    * Add "lisa-sets / compile" and "lisa-examples / compile" to the CI.
    70059505
    Atomics, improve lisa.fol.FOL's logic and simplify it (#194)
    SimonGuilloud authored
    * Renamed some elements of the formula hierarchy using the word "atomic"
    
    * removed the match type for ***. Instead, use opaque types and extension methods. Should be a bit more efficient and less prone to dotty bugs
    
    * remove ***. Only ** left
    
    * removing apply for sequences (use applyUnsafe)
    
    * mostly good but one theorem doesn't pass anymore
    
    * everything goes, no more *** (i.e. no match type)
    
    * progress
    
    * PredKer
    
    * mend
    
    * ConstantAtomicLabel, AtomicFormula
    
    * All atomic renaming completed
    
    * back to compile
    
    * finished tests, removed ConsOrPred
    
    * next step: Removes contravariant labels and terms and formulas extending |->
    
    * finish predicates, compiles
    
    * progress, Binders to sort and organize, some renaming to do in other files. Can remove - in labels.
    
    * finished cleaning and uniformizing definitions in Commons.scala, adapted other files accordingly. Compiles, tests passes, formated.
    
    * re-checked some warning, removed some redundant type checks.
    
    * fix substituteUnsafe2
    
    * Add "lisa-sets / compile" and "lisa-examples / compile" to the CI.
Loading