Skip to content
Snippets Groups Projects
user avatar
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
History
Name Last commit Last update
..
src/main/scala/lisa/kernel