Idris.Elab.Rewrite

Documentation

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

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

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