License	BSD3
Maintainer	The Idris Community.
Safe Haskell	None
Language	Haskell2010

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...)