git.iko.soy/Idris-dev
on master help sign in
fix reference
5267e39Martin Baker
docs/proofs/tactics.rst+2−2
compare with master
unifiedsplit
@@ -8,7 +8,7 @@ Before looking at the Elab monad we need to know how to construct terms.
8Holes
8Holes
9=====
9=====
10
10
11−For more information about holes and guesses see `Dependently Typed Functional Programs and their Proofs McBride 1999`_.
11+For more information about holes and guesses see `Dependently Typed Functional Programs and their Proofs by McBride 1999`_.
12
12
13Proof State
13Proof State
14===========
14===========
@@ -436,4 +436,4 @@ However this would cause the application of f to be ill-typed, as it expects an
436 letbind : (n : TTName) -> (ty, tm : Raw) -> Elab ()
436 letbind : (n : TTName) -> (ty, tm : Raw) -> Elab ()
437
437
438... target-notes::
438... target-notes::
439−. _`Dependently Typed Functional Programs and their Proofs McBride 1999`: https://www.era.lib.ed.ac.uk/handle/1842/374
439+. _`Dependently Typed Functional Programs and their Proofs by McBride 1999`: https://www.era.lib.ed.ac.uk/handle/1842/374