| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Opacity
Synopsis
- saturateOpaqueBlocks :: forall m. (MonadTCState m, ReadTCState m, MonadFresh OpaqueId m, MonadDebug m, MonadTrace m, MonadWarning m, MonadIO m) => [Declaration] -> m ()
- isAccessibleDef :: TCEnv -> TCState -> Definition -> Bool
- hasAccessibleDef :: (ReadTCState m, MonadTCEnv m, HasConstInfo m) => QName -> m Bool
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?