@@ -419,14 +419,6 @@ Read and Write State
419419
420420 lookupFunDefnExact : TTName -> Elab (FunDefn TT)
421421
422− .. code-block:: idris
423−
424− lookupFunDefnExact n = case !(lookupFunDefn n) of
425− [res] => pure res
426− [] => fail [TextPart
427− "No function named", NamePart n]
428− xs => fail [TextPart "More than one function named",
429− NamePart n]
430422 * - lookupArgs
431423 - Get the argument specification for each overloading of a name.
432424
@@ -443,11 +435,6 @@ Read and Write State
443435
444436 .. code-block:: idris
445437
446− lookupArgsExact n = case !(lookupArgs n) of
447− [res] => pure res
448− [] => fail [NamePart n, TextPart "is not defined."]
449− xs => fail [NamePart n, TextPart "is ambiguous."]
450−
451438 * - check
452439 - Attempt to type-check a term, getting back itself and its type.
453440