idris- Functional Programming Language with Dependent Types

Safe HaskellNone




data ElabMode Source




resolveTC :: Bool -> Int -> Term -> Name -> IState -> ElabD () Source

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

case_ :: Bool -> Bool -> IState -> Name -> PTerm -> ElabD () Source

reflm :: String -> Name Source

Prefix a name with the Language.Reflection namespace

reify :: IState -> Term -> ElabD PTactic Source

Reify tactics from their reflected representation

reifyTT :: Term -> ElabD Term Source

Reify terms from their reflected representation

reifyRaw :: Term -> ElabD Raw Source

Reify raw terms from their reflected representation

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

Create a reflected call to a named function/constructor

reflect :: Term -> Raw Source

Lift a term into its Language.Reflection.TT representation

reflectQuotePattern :: [Name] -> Term -> ElabD () Source

Convert a reflected term to a more suitable form for pattern-matching. In particular, the less-interesting bits are elaborated to _ patterns. This happens to NameTypes, universe levels, names that are bound but not used, and the type annotation field of the P constructor.

reflectQuote :: [Name] -> Term -> Raw Source

Create a reflected term, but leave refs to the provided name intact

reflectNameQuotePattern :: Name -> ElabD () Source

Elaborate a name to a pattern. This means that NS and UN will be intact. MNs corresponding to will care about the string but not the number. All others become _.

mkList :: Raw -> [Raw] -> Raw Source

reflectEnv :: Env -> Raw Source

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

rawBool :: Bool -> Raw Source

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

rawCons :: Raw -> Raw -> Raw -> Raw Source

rawList :: Raw -> [Raw] -> Raw Source

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

reifyReportPart :: Term -> Either Err ErrorReportPart Source

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.