Agda-2.6.3.20230930: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.TypeChecking.Rules.LHS.Unify.LeftInverse

Documentation

data NoLeftInv Source #

Constructors

UnsupportedYet 

Fields

Illegal 

Fields

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 #