idris-1.3.4: Functional Programming Language with Dependent Types
LicenseBSD3
MaintainerThe Idris Community.
Safe HaskellSafe-Inferred
LanguageHaskell2010

Idris.Elab.Rewrite

Description

 
Synopsis

Documentation

elabRewrite :: (PTerm -> ElabD ()) -> IState -> FC -> Maybe Name -> PTerm -> PTerm -> Maybe PTerm -> ElabD () Source #

elabRewriteLemma :: ElabInfo -> Name -> Type -> Idris () Source #

Make a rewriting lemma for the given type constructor.

If it fails, fail silently (it may well fail for some very complex types. We can fix this later, for now this gives us a lot more working rewrites...)