@@ -426,5 +426,5 @@ However this would cause the application of f to be ill-typed, as it expects an
427 letbind : (n : TTName) -> (ty, tm : Raw) -> Elab ()
427 letbind : (n : TTName) -> (ty, tm : Raw) -> Elab ()
429−... target-notes::
429+.. target-notes::
430−. _`Dependently Typed Functional Programs and their Proofs by McBride 1999`: https://www.era.lib.ed.ac.uk/handle/1842/374
430+.. _`Dependently Typed Functional Programs and their Proofs by McBride 1999`: https://www.era.lib.ed.ac.uk/handle/1842/374