@@ -419,14 +419,6 @@ Read and Write State
420 lookupFunDefnExact : TTName -> Elab (FunDefn TT)
420 lookupFunDefnExact : TTName -> Elab (FunDefn TT)
422− .. code-block:: idris
424− lookupFunDefnExact n = case !(lookupFunDefn n) of
426− [] => fail [TextPart
427− "No function named", NamePart n]
428− xs => fail [TextPart "More than one function named",
430 * - lookupArgs
422 * - lookupArgs
431 - Get the argument specification for each overloading of a name.
423 - Get the argument specification for each overloading of a name.
@@ -443,11 +435,6 @@ Read and Write State
444 .. code-block:: idris
436 .. code-block:: idris
446− lookupArgsExact n = case !(lookupArgs n) of
448− [] => fail [NamePart n, TextPart "is not defined."]
449− xs => fail [NamePart n, TextPart "is ambiguous."]
451 * - check
438 * - check
452 - Attempt to type-check a term, getting back itself and its type.
439 - Attempt to type-check a term, getting back itself and its type.