Skip to content

HORIZON HASKELL Docs lts/ghc-10.0.xd29e1592026-10-12Search names, modules, packages, or :: a typeCtrl K

GHC 10.0.0.20260917 · lts/ghc-10.0.x · d29e159 · 2026-10-12

ModuleAgda-2.8.0.2Haskell2010

Agda.TypeChecking.Rules.LHS.Unify.LeftInverse

2 types
5 values

PackageAgda-2.8.0.2
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.8.0.2 · Agda.TypeChecking.Rules.LHS.Unify.LeftInverse
PrettyTCM NoLeftInvDefined in Agda-2.8.0.2 · 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