Idris.ElabDecls

Synopsis

• recheckC :: FC -> Env -> TT Name -> StateT IState (ErrorT Err IO) (Term, Type)
• checkDef :: FC -> [(t, (t1, t2, TT Name))] -> StateT IState (ErrorT Err IO) [(t, (t1, t2, Term))]
• elabType :: ElabInfo -> SyntaxInfo -> String -> FC -> FnOpts -> Name -> PTerm -> Idris Type
• elabType' :: Bool -> ElabInfo -> SyntaxInfo -> String -> FC -> FnOpts -> Name -> PTerm -> Idris Type
• elabPostulate :: ElabInfo -> SyntaxInfo -> String -> FC -> FnOpts -> Name -> PTerm -> Idris ()
• elabData :: ElabInfo -> SyntaxInfo -> String -> FC -> Bool -> PData -> Idris ()
• elabPrims :: Idris ()
• elabProvider :: ElabInfo -> SyntaxInfo -> FC -> Name -> PTerm -> PTerm -> Idris ()
• elabTransform :: ElabInfo -> FC -> Bool -> PTerm -> PTerm -> Idris ()
• elabRecord :: ElabInfo -> SyntaxInfo -> String -> FC -> Name -> PTerm -> String -> Name -> PTerm -> Idris ()
• elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool -> (String, Name, PTerm, FC) -> 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
• elabClause :: ElabInfo -> FnOpts -> (Int, PClause) -> Idris (Either Term (Term, Term))
• data MArgTy
  • = IA
  • | EA
  • | CA
• elabClass :: ElabInfo -> SyntaxInfo -> String -> FC -> [PTerm] -> Name -> [(Name, PTerm)] -> [PDecl] -> Idris ()
• elabInstance :: ElabInfo -> SyntaxInfo -> FC -> [PTerm] -> Name -> [PTerm] -> PTerm -> Maybe Name -> [PDecl] -> Idris ()
• decorateid :: (Name -> Name) -> PDecl' PTerm -> PDecl' PTerm
• pbinds :: TT Name -> StateT (ElabState aux) TC ()
• 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

Documentation