| Copyright | License : BSD3 |
|---|---|
| Maintainer | The Idris Community. |
| Safe Haskell | None |
| Language | Haskell98 |
Idris.Elab.Clause
Description
- elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()
- elabPE :: ElabInfo -> FC -> Name -> Term -> Idris [(Term, Term)]
- checkPossible :: ElabInfo -> FC -> Bool -> Name -> PTerm -> Idris Bool
- findUnique :: Context -> Env -> Term -> [Name]
- elabClause :: ElabInfo -> FnOpts -> (Int, PClause) -> Idris (Either Term (Term, Term), PTerm)
- mapRHS :: (PTerm -> PTerm) -> PClause -> PClause
- mapRHSdecl :: (PTerm -> PTerm) -> PDecl -> PDecl
Documentation
elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris () Source #
Elaborate a collection of left-hand and right-hand pairs - that is, a top-level definition.
elabPE :: ElabInfo -> FC -> Name -> Term -> Idris [(Term, Term)] Source #
Find static applications in a term and partially evaluate them.
Return any new transformation rules
checkPossible :: ElabInfo -> FC -> Bool -> Name -> PTerm -> Idris Bool Source #
Checks if the clause is a possible left hand side.
elabClause :: ElabInfo -> FnOpts -> (Int, PClause) -> Idris (Either Term (Term, Term), PTerm) Source #
Return the elaborated LHS/RHS, and the original LHS with implicits added