Idris.Elab.Clause

Documentation

elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()

Elaborate a collection of left-hand and right-hand pairs - that is, a top-level definition.

elabPE :: ElabInfo -> FC -> Name -> Term -> Idris [(Term, Term)]

Find static applications in a term and partially evaluate them. Return any new transformation rules

checkPossible :: ElabInfo -> FC -> Bool -> Name -> PTerm -> Idris Bool

Checks if the clause is a possible left hand side.

propagateParams :: IState -> [Name] -> Type -> [Name] -> PTerm -> PTerm

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