Untitled Document3. Arithmetic omega - Presburger arithmetic (propositional formulas, with equalities, inequalities, for nat and Z) auto with arith - ring - associative commutative rewriting field - equalities in commutative fields (like ring, but with division) fourier - linear inequations with propositional structure, on real numbers 4. Induction Introduction (prove inductive facts) apply - treat each constructo
Algebra of programming using dependent types | Lambda the Ultimate
