Agda.TypeChecking.Rules.LHS.Unify.LeftInverse

Documentation

data NoLeftInv

Constructors

UnsupportedYet

Fields

• badStep :: UnifyStep

Illegal

Fields

• badStep :: UnifyStep

NoCubical

WithKEnabled

SplitOnStrict

splitting on a Strict Set.

SplitOnFlat

splitting on a @♭ argument

UnsupportedCxt

Instances

PrettyTCM NoLeftInv

Defined in Agda.TypeChecking.Rules.LHS.Unify.LeftInverse

Methods

prettyTCM :: MonadPretty m => NoLeftInv -> m Doc

Show NoLeftInv

Defined in Agda.TypeChecking.Rules.LHS.Unify.LeftInverse

Methods

showsPrec :: Int -> NoLeftInv -> ShowS

show :: NoLeftInv -> String

showList :: [NoLeftInv] -> ShowS

buildLeftInverse :: (PureTCM tcm, MonadError TCErr tcm) => UnifyState -> UnifyLog -> tcm (Either NoLeftInv (Substitution, Substitution))

type Retract = (Telescope, Substitution, Substitution, Substitution)

termsS :: DeBruijn a => Impossible -> [a] -> Substitution' a

composeRetract :: (PureTCM tcm, MonadError TCErr tcm, MonadDebug tcm, HasBuiltins tcm, MonadAddContext tcm) => Retract -> Term -> Retract -> tcm Retract

buildEquiv :: forall tcm. (PureTCM tcm, MonadError TCErr tcm) => UnifyLogEntry -> UnifyState -> tcm (Either NoLeftInv (Retract, Term))

explainStep :: MonadPretty m => UnifyStep -> m Doc