idris-0.9.12: Functional Programming Language with Dependent Types

Safe HaskellNone




data ElabInfo Source




params :: [(Name, PTerm)]
inblock :: Ctxt [Name]
liftname :: Name -> Name
namespace :: Maybe [String]

resTC' :: (Eq a, Num a) => [TT Name] -> a -> Term -> Name -> IState -> StateT (ElabState [PDecl]) TC ()Source

reflm :: String -> NameSource

Prefix a name with the Language.Reflection namespace

reify :: IState -> Term -> ElabD PTacticSource

Reify tactics from their reflected representation

reifyTT :: Term -> ElabD TermSource

Reify terms from their reflected representation

reifyRaw :: Term -> ElabD RawSource

Reify raw terms from their reflected representation

reflCall :: String -> [Raw] -> RawSource

Create a reflected call to a named function/constructor

reflect :: Term -> RawSource

Lift a term into its Language.Reflection.TT representation

reflectEnv :: Env -> RawSource

Reflect the environment of a proof into a List (TTName, Binder TT)

rawBool :: Bool -> RawSource

Reflect an error into the internal datatype of Idris -- TODO

rawPair :: (Raw, Raw) -> (Raw, Raw) -> RawSource

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.