Theories

Created by: SimonGuilloud

New canonical style to write theories. An example :

object SetTheory extends proven.Main {

THEOREM("russelParadox") of "∀x. (x ∈ ?y) ↔ ¬(x ∈ x) ⊢" PROOF { .... } using () thm"russelParadox".show

THEOREM("unorderedPair_symmetry") of "⊢ ∀y, x. {x, y} = {y, x}" PROOF { ... } using (ax"extensionalityAxiom", ax"pairAxiom") show

val oPair: ConstantFunctionLabel = DEFINE("", sx, sy) as pair(pair(sx, sy), pair(sx, sx)) show

}

Friendly, explicit and hopefully intuitive syntax to write theorems and definitions. Can run theory file, and only outputs of this file gets printed (instead of everything that is initialised). High number of various helpers, implicit conversions and syntactic sugar.

Essentially documented.