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

Safe Haskell	Safe-Inferred
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 show :: NoLeftInv -> String showList :: [NoLeftInv] -> ShowS

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 :: forall tcm. (PureTCM tcm, MonadError TCErr tcm) => UnifyLogEntry -> UnifyState -> tcm (Either NoLeftInv (Retract, Term)) Source #

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