From 1257313e9485788df6e59a939563cf50af054bb4 Mon Sep 17 00:00:00 2001 From: Raphael Cauderlier Date: Fri, 2 Feb 2018 15:51:36 +0100 Subject: [PATCH] Fix links in the manual --- manual.org | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/manual.org b/manual.org index eadff69..77e9fc9 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 -- 2.24.1