Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Opacity

Synopsis

- saturateOpaqueBlocks :: (MonadTCState m, ReadTCState m, MonadFresh OpaqueId m, MonadDebug m, MonadTrace m, MonadWarning m, MonadIO m) => m ()
- isAccessibleDef :: TCEnv -> TCState -> Definition -> Bool
- hasAccessibleDef :: (ReadTCState m, MonadTCEnv m, HasConstInfo m) => QName -> m Bool

# Documentation

saturateOpaqueBlocks :: (MonadTCState m, ReadTCState m, MonadFresh OpaqueId m, MonadDebug m, MonadTrace m, MonadWarning m, MonadIO m) => 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`?