idris-0.99.2: Functional Programming Language with Dependent Types

CopyrightLicense : BSD3
MaintainerThe Idris Community.
Safe HaskellNone
LanguageHaskell98

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