idris-0.9.17: Functional Programming Language with Dependent Types

Safe HaskellNone
LanguageHaskell98

Idris.Elab.Clause

Synopsis

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