Commit 1257313e by Raphael Cauderlier

### Fix links in the manual

parent 39843a8a
 ... ... @@ -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 ... ...
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment