Idris.ElabTerm

Synopsis

• data ElabInfo = EInfo {
  • params :: [(Name, PTerm)]
  • inblock :: Ctxt [Name]
  • liftname :: Name -> Name
  • namespace :: Maybe [String]
  }
• toplevel :: ElabInfo
• build :: IState -> ElabInfo -> Bool -> Name -> PTerm -> ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl])
• buildTC :: IState -> ElabInfo -> Bool -> Bool -> Name -> PTerm -> ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl])
• elab :: IState -> ElabInfo -> Bool -> Bool -> Name -> PTerm -> ElabD ()
• pruneAlt :: [PTerm] -> [PTerm]
• pruneByType :: Term -> Context -> [PTerm] -> [PTerm]
• findInstances :: IState -> Term -> [Name]
• trivial' :: IState -> ElabD ()
• proofSearch' :: IState -> Maybe Name -> Name -> [Name] -> ElabD ()
• resolveTC :: Int -> Name -> IState -> ElabD ()
• collectDeferred :: Maybe Name -> Term -> State [(Name, (Int, Maybe Name, Type))] Term
• runTac :: Bool -> IState -> PTactic -> ElabD ()
• reflm :: String -> Name
• reify :: IState -> Term -> ElabD PTactic
• reifyApp :: IState -> Name -> [Term] -> ElabD PTactic
• reifyTT :: Term -> ElabD Term
• reifyTTApp :: Name -> [Term] -> ElabD Term
• reifyRaw :: Term -> ElabD Raw
• reifyRawApp :: Name -> [Term] -> ElabD Raw
• reifyTTName :: Term -> ElabD Name
• reifyTTNameApp :: Name -> [Term] -> ElabD Name
• reifyTTNamespace :: Term -> ElabD [String]
• reifyTTNameType :: Term -> ElabD NameType
• reifyTTBinder :: (Term -> ElabD a) -> Name -> Term -> ElabD (Binder a)
• reifyTTBinderApp :: (Term -> ElabD a) -> Name -> [Term] -> ElabD (Binder a)
• reifyTTConst :: Term -> ElabD Const
• reifyTTConstApp :: Name -> Term -> ElabD Const
• reifyTTUExp :: Term -> ElabD UExp
• reflCall :: String -> [Raw] -> Raw
• reflect :: Term -> Raw
• reflectNameType :: NameType -> Raw
• reflectName :: Name -> Raw
• reflectBinder :: Binder Term -> Raw
• reflectConstant :: Const -> Raw
• reflectUExp :: UExp -> Raw
• reflectEnv :: Env -> Raw
• reflectErr :: Err -> Raw
• envTupleType :: Raw
• solveAll :: Elab' aux ()
• mkSpecialised :: IState -> FC -> Name -> [PTerm] -> PTerm -> ElabD PTerm
• mkSpecDecl :: IState -> Name -> [(PTerm, Bool)] -> PTerm -> ElabD PTerm

Documentation