Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Rules.LHS.Unify.LeftInverse

# Documentation

data NoLeftInv Source #

Constructors

UnsupportedYet |

Fields

- badStep :: UnifyStep

Illegal |

Fields

- badStep :: UnifyStep

NoCubical |
WithKEnabled |
SplitOnStrict | splitting on a Strict Set.
SplitOnFlat | splitting on a @♭ argument
UnsupportedCxt |

#### Instances

Instances details

PrettyTCM NoLeftInv Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Unify.LeftInverse Methods prettyTCM :: MonadPretty m => NoLeftInv -> m Doc Source #
Show NoLeftInv Source # |
Instance details Defined in Agda.TypeChecking.Rules.LHS.Unify.LeftInverse Methods showsPrec :: Int -> NoLeftInv -> ShowS Source # show :: NoLeftInv -> String Source # showList :: [NoLeftInv] -> ShowS Source #

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 #