formula list ClassicalProps(jlc) Doc

Sections needed for formula_list

formula list
sequent equality
sequent
formula validity
full assignment
sat lemmas
formula equality
formula rank
formula falsification
formula satisfaction
valuation
formulaPropositional formula structure.
KleeneKleene 3-valued truth connectives.
assignment
ThreeType of 3-truth-values
var jlc
list 3 jlcMore on Lists
core 3 jlcVarious facts about Propositional Operators
discrete jlcBasics of Discrete Types
bool 2 jlcA few basic facts about asserting Bools and Bool Equalities
lambda jlcCurrying functions and Explicitly expressing recursion.
list 1
int 2Defines mod, floor, max and min functions over the integers. Lemmas concern basic properties of arithmetic functions over integers, and induction principles.
rfunction 1
prog 1
sqequal 1
quot 1Support lemmas for quotient type.
rel 1Common properties of binary relations.
unionNon canonical functions (isl, outl, outr) for union type.
bool 1Definitions, theorems and tactics for the boolean type and boolean-related expressions.
int 1Integer inequalities, subtypes, and induction lemmas for subtypes.
well fndWell-founded predicate. Rank induction lemmas and tactics.
fun 1Polymorphic identity and composition functions. Lemmas covering properties such as injectivity and surjectivity.
coreSome basic concepts defined type-theoretically.