| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Rules.LHS.Unify.LeftInverse
Documentation
Constructors
| UnsupportedYet | |
| Illegal | |
| NoCubical | |
| WithKEnabled | |
| SplitOnStrict | splitting on a Strict Set. |
| SplitOnFlat | splitting on a @♭ argument |
| UnsupportedCxt | |
buildLeftInverse :: (PureTCM tcm, MonadError TCErr tcm) => UnifyState -> UnifyLog -> tcm (Either NoLeftInv (Substitution, Substitution)) Source #
type Retract = (Telescope, Substitution, Substitution, Substitution) Source #
termsS :: DeBruijn a => Impossible -> [a] -> Substitution' a Source #
composeRetract :: (PureTCM tcm, MonadError TCErr tcm, MonadDebug tcm, HasBuiltins tcm, MonadAddContext tcm) => Retract -> Term -> Retract -> tcm Retract Source #
buildEquiv :: (PureTCM tcm, MonadError TCErr tcm) => UnifyLogEntry -> UnifyState -> tcm (Either NoLeftInv (Retract, Term)) Source #
explainStep :: MonadPretty m => UnifyStep -> m Doc Source #