From 4b45cda6f14f53871c0824cca755060daedce618 Mon Sep 17 00:00:00 2001 From: Jeehoon Kang Date: Fri, 22 Jan 2016 17:42:10 -0500 Subject: [PATCH] fix(02): link --- 02_Dependent_Type_Theory.org | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/02_Dependent_Type_Theory.org b/02_Dependent_Type_Theory.org index 7b569bbf..cf655e14 100644 --- a/02_Dependent_Type_Theory.org +++ b/02_Dependent_Type_Theory.org @@ -1217,7 +1217,7 @@ Notice that now the first =check= command gives the type of the identifier, =ident=, without inserting any placeholders. Moreover, the output indicates that the first argument is implicit. -Section [[file:08_Building_Theories_and_Proof::#More_on_Implicit_Arguments][More on Implicit Arguments]] explains another useful annotation, +Section [[file:08_Building_Theories_and_Proofs.org::#More_on_Implicit_Arguments][More on Implicit Arguments]] explains another useful annotation, =!=, which makes explicit arguments implicit. In a sense, it is the opposite of =@=, and is most useful in the context of theorem proving, which we will turn to next.