Idris.Elab.Term

Synopsis

• data ElabMode
  • = ETyDecl
  • | ETransLHS
  • | ELHS
  • | ERHS
• data ElabResult = ElabResult {
  • resultTerm :: Term
  • resultMetavars :: [(Name, (Int, Maybe Name, Type, [Name]))]
  • resultCaseDecls :: [PDecl]
  • resultContext :: Context
  • resultTyDecls :: [RDeclInstructions]
  • resultHighlighting :: [(FC, OutputAnnotation)]
  }
• build :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm -> ElabD ElabResult
• buildTC :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm -> ElabD ElabResult
• getUnmatchable :: Context -> Name -> [Bool]
• data ElabCtxt = ElabCtxt {
  • e_inarg :: Bool
  • e_isfn :: Bool
  • e_guarded :: Bool
  • e_intype :: Bool
  • e_qq :: Bool
  • e_nomatching :: Bool
  }
• initElabCtxt :: ElabCtxt
• goal_polymorphic :: ElabD Bool
• elab :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm -> ElabD ()
• pruneAlt :: [PTerm] -> [PTerm]
• pruneByType :: Env -> Term -> IState -> [PTerm] -> [PTerm]
• isPlausible :: IState -> Bool -> Env -> Name -> Type -> Bool
• findHighlight :: Name -> ElabD OutputAnnotation
• solveAuto :: IState -> Name -> Bool -> Name -> ElabD ()
• solveAutos :: IState -> Name -> Bool -> ElabD ()
• trivial' :: IState -> ElabD ()
• trivialHoles' :: [Name] -> [(Name, Int)] -> IState -> ElabD ()
• proofSearch' :: IState -> Bool -> Bool -> Int -> Bool -> Maybe Name -> Name -> [Name] -> [Name] -> StateT (ElabState EState) TC ()
• resolveTC' :: Bool -> Bool -> Int -> Term -> Name -> IState -> ElabD ()
• collectDeferred :: Maybe Name -> [Name] -> Context -> Term -> State [(Name, (Int, Maybe Name, Type, [Name]))] Term
• case_ :: Bool -> Bool -> IState -> Name -> PTerm -> ElabD ()
• metavarName :: Maybe [String] -> Name -> Name
• runElabAction :: IState -> FC -> Env -> Term -> [String] -> ElabD Term
• runTac :: Bool -> IState -> Maybe FC -> Name -> PTactic -> ElabD ()
• elaboratingArgErr :: [(Name, Name)] -> Err -> Err
• withErrorReflection :: Idris a -> Idris a
• solveAll :: Elab' aux ()
• processTacticDecls :: ElabInfo -> [RDeclInstructions] -> Idris ()

Documentation