Skip to content

HORIZON HASKELL Docs lts/ghc-9.10.x248f8f02026-10-05Search names, modules, packages, or :: a typeCtrl K

GHC 9.10.3 · lts/ghc-9.10.x · 248f8f0 · 2026-10-05

ModuleAgda-2.7.0.1Haskell2010

Agda.TypeChecking.Rules.LHS.Unify.LeftInverse

2 types
5 values

PackageAgda-2.7.0.1
Exports7
LanguageHaskell2010
LicenceMIT

datadata NoLeftInv

Constructors

UnsupportedYet
- badStep :: UnifyStep
Illegal
- badStep :: UnifyStep
NoCubical
WithKEnabled
SplitOnStrict
splitting on a Strict Set.
SplitOnFlat
splitting on a @♭ argument
UnsupportedCxt

Instances2Show, PrettyTCM

Show NoLeftInvDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS.Unify.LeftInverse
PrettyTCM NoLeftInvDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS.Unify.LeftInverse

valuebuildLeftInverse

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

typetype Retract = (Telescope, Substitution, Substitution, Substitution)

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

valuecomposeRetract

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

valuebuildEquiv

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

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