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

Agda.TypeChecking.Opacity

Synopsis

Documentation

saturateOpaqueBlocks :: forall m. (MonadTCState m, ReadTCState m, MonadFresh OpaqueId m, MonadDebug m, MonadTrace m, MonadWarning m, MonadIO m) => [Declaration] -> m () Source #

Ensure that opaque blocks defined in the current module have saturated unfolding sets.

isAccessibleDef :: TCEnv -> TCState -> Definition -> Bool Source #

Decide whether or not a definition is reducible. Returns True if the definition can step.

hasAccessibleDef :: (ReadTCState m, MonadTCEnv m, HasConstInfo m) => QName -> m Bool Source #

Will the given QName have a proper definition, or will it be wrapped in an AbstractDefn?