@@ -8,7 +8,7 @@ Before looking at the Elab monad we need to know how to construct terms.
88Holes
99=====
1010
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`_.
1212
1313Proof State
1414===========
@@ -436,4 +436,4 @@ However this would cause the application of f to be ill-typed, as it expects an
436436 letbind : (n : TTName) -> (ty, tm : Raw) -> Elab ()
437437
438438... 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