Agda-2.6.4: 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

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 #

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 #