Idris.ElabDecls

Synopsis

• recheckC :: FC -> Env -> TT Name -> StateT IState (ErrorT Err IO) (Term, Type)
• checkDef :: FC -> [(Name, (Int, Maybe Name, TT Name))] -> StateT IState (ErrorT Err IO) [(Name, (Int, Maybe Name, Term))]
• checkAddDef :: Bool -> Bool -> FC -> [(Name, (Int, Maybe Name, TT Name))] -> StateT IState (ErrorT Err IO) [(Name, (Int, Maybe Name, Term))]
• elabType :: ElabInfo -> SyntaxInfo -> Docstring -> [(Name, Docstring)] -> FC -> FnOpts -> Name -> PTerm -> Idris Type
• elabType' :: Bool -> ElabInfo -> SyntaxInfo -> Docstring -> [(Name, Docstring)] -> FC -> FnOpts -> Name -> PTerm -> Idris Type
• elabPostulate :: ElabInfo -> SyntaxInfo -> Docstring -> FC -> FnOpts -> Name -> PTerm -> Idris ()
• elabData :: ElabInfo -> SyntaxInfo -> Docstring -> [(Name, Docstring)] -> FC -> DataOpts -> PData -> Idris ()
• type EliminatorState = StateT (Map String Int) Idris
• elabEliminator :: [Int] -> Name -> PTerm -> [(Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name])] -> ElabInfo -> EliminatorState ()
• elabPrims :: Idris ()
• elabProvider :: ElabInfo -> SyntaxInfo -> FC -> ProvideWhat -> Name -> PTerm -> PTerm -> Idris ()
• elabTransform :: ElabInfo -> FC -> Bool -> PTerm -> PTerm -> Idris ()
• elabRecord :: ElabInfo -> SyntaxInfo -> Docstring -> FC -> Name -> PTerm -> Docstring -> Name -> PTerm -> Idris ()
• elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool -> (Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name]) -> Idris (Name, Type)
• elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()
• elabPE :: ElabInfo -> FC -> Name -> Term -> Idris ()
• elabValBind :: ElabInfo -> Bool -> PTerm -> Idris (Term, Type, [(Name, Type)])
• elabVal :: ElabInfo -> Bool -> PTerm -> Idris (Term, Type)
• checkPossible :: ElabInfo -> FC -> Bool -> Name -> PTerm -> Idris Bool
• getFixedInType :: IState -> [Name] -> [PArg' t] -> TT Name -> [Name]
• getFlexInType :: IState -> [Name] -> [Name] -> TT Name -> [Name]
• getParamsInType :: IState -> [Name] -> [PArg' t] -> TT Name -> [Name]
• paramNames :: Eq a => [TT a] -> [a] -> [Int] -> [a]
• propagateParams :: [Name] -> Type -> PTerm -> PTerm
• elabClause :: ElabInfo -> FnOpts -> (Int, PClause) -> Idris (Either Term (Term, Term), PTerm)
• data MArgTy
  • = IA
  • | EA
  • | CA
• elabClass :: ElabInfo -> SyntaxInfo -> Docstring -> FC -> [PTerm] -> Name -> [(Name, PTerm)] -> [PDecl] -> Idris ()
• elabInstance :: ElabInfo -> SyntaxInfo -> ElabWhat -> FC -> [PTerm] -> Name -> [PTerm] -> PTerm -> Maybe Name -> [PDecl] -> Idris ()
• decorateid :: (Name -> Name) -> PDecl' PTerm -> PDecl' PTerm
• pbinds :: IState -> Term -> ElabD ()
• pbty :: TT n -> TT n -> TT n
• getPBtys :: TT t -> [(t, TT t)]
• psolve :: TT t -> StateT (ElabState aux) TC ()
• pvars :: IState -> TT Name -> [(Name, PTerm)]
• data ElabWhat
  • = ETypes
  • | EDefns
  • | EAll
• elabDecls :: ElabInfo -> [PDecl] -> Idris ()
• elabDecl :: ElabWhat -> ElabInfo -> PDecl -> Idris ()
• elabDecl' :: ElabWhat -> ElabInfo -> PDecl' PTerm -> StateT IState (ErrorT Err IO) ()
• elabCaseBlock :: ElabInfo -> [FnOpt] -> PDecl' PTerm -> StateT IState (ErrorT Err IO) ()
• checkInferred :: FC -> PTerm -> PTerm -> Idris ()
• inferredDiff :: FC -> PTerm -> PTerm -> Idris Bool
• checkDocs :: FC -> [(Name, Docstring)] -> PTerm -> Idris ()

Documentation