Safe Haskell | None |
---|
- data ElabInfo = EInfo {}
- toplevel :: ElabInfo
- build :: IState -> ElabInfo -> Bool -> FnOpts -> Name -> PTerm -> ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl])
- buildTC :: IState -> ElabInfo -> Bool -> FnOpts -> Name -> PTerm -> ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl])
- elab :: IState -> ElabInfo -> Bool -> FnOpts -> Name -> PTerm -> ElabD ()
- reflectFunctionErrors :: IState -> Name -> Name -> ElabD a -> ElabD a
- pruneAlt :: [PTerm] -> [PTerm]
- pruneByType :: Term -> Context -> [PTerm] -> [PTerm]
- findInstances :: IState -> Term -> [Name]
- trivial' :: IState -> ElabD ()
- proofSearch' :: IState -> Maybe Name -> Name -> [Name] -> ElabD ()
- resolveTC :: Int -> Term -> 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
- rawBool :: Bool -> Raw
- rawNil :: Raw -> Raw
- rawCons :: Raw -> Raw -> Raw -> Raw
- rawList :: Raw -> [Raw] -> Raw
- rawPairTy :: Raw -> Raw -> Raw
- rawPair :: (Raw, Raw) -> (Raw, Raw) -> Raw
- reflectCtxt :: [(Name, Type)] -> Raw
- reflectErr :: Err -> Raw
- withErrorReflection :: Idris a -> Idris a
- fromTTMaybe :: Term -> Maybe Term
- reflErrName :: String -> Name
- reifyReportPart :: Term -> Either Err ErrorReportPart
- envTupleType :: Raw
- solveAll :: Elab' aux ()
Documentation
build :: IState -> ElabInfo -> Bool -> FnOpts -> Name -> PTerm -> ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl])Source
buildTC :: IState -> ElabInfo -> Bool -> FnOpts -> Name -> PTerm -> ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl])Source
reflectFunctionErrors :: IState -> Name -> Name -> ElabD a -> ElabD aSource
Perform error reflection for function applicaitons with specific error handlers
findInstances :: IState -> Term -> [Name]Source
Prefix a name with the Language.Reflection namespace
reifyTTName :: Term -> ElabD NameSource
reifyTTNamespace :: Term -> ElabD [String]Source
reifyTTConst :: Term -> ElabD ConstSource
reifyTTUExp :: Term -> ElabD UExpSource
reflectNameType :: NameType -> RawSource
reflectName :: Name -> RawSource
reflectBinder :: Binder Term -> RawSource
reflectConstant :: Const -> RawSource
reflectUExp :: UExp -> RawSource
reflectEnv :: Env -> RawSource
Reflect the environment of a proof into a List (TTName, Binder TT)
reflectCtxt :: [(Name, Type)] -> RawSource
reflectErr :: Err -> RawSource
withErrorReflection :: Idris a -> Idris aSource
fromTTMaybe :: Term -> Maybe TermSource
reflErrName :: String -> NameSource
reifyReportPart :: Term -> Either Err ErrorReportPartSource
Attempt to reify a report part from TT to the internal representation. Not in Idris or ElabD monads because it should be usable from either.