diff --git a/manual.org b/manual.org index eadff69a7efd51df35e595a79b317edf7a2011d7..77e9fc9a5694b5204a13374106426c6502090eac 100644 --- a/manual.org +++ b/manual.org @@ -200,8 +200,7 @@ function =fol.proof= is defined using an impredicative encoding but we usually do not use the definition directly but rather rely on the following theorems proved in the file [[./fol/fol.dk][fol/fol.dk]] and representing natural deduction introduction and elimination rules (or the -corresponding certificates constructors presented in [[* Reasoning][the reasoning -section]]): +corresponding certificates constructors presented in [[* Reasoning][the reasoning section]]): - =fol.false_elim : A : fol.prop -> fol.proof fol.false -> fol.proof A= - =fol.true_intro : fol.proof fol.true= - =fol.and_intro : A : fol.prop -> B : fol.prop -> fol.proof A -> fol.proof B -> fol.proof (fol.and A B)= @@ -634,7 +633,7 @@ proves =eq.eq A b c=. The certificate =eqcert.f_equal f c1 … cn= proves =eq.eq B (fol.fun_apply f a1 … an) (fol.fun_apply f a1' … an')= if each =ci= proves =eq.eq Ai ai ai'=. The certificate =eqcert.rewrite A a a' c1 c2= proves =B= if =c1= proves =eq.eq A a a'= and =c2= proves -=B= in which each occurrence of =a= has been replaced by =a'= (see [[* Substitution and unification][the +=B= in which each occurrence of =a= has been replaced by =a'= (see [[* Substitutions][the section on substitution]]). ** Classical Reasoning