EncodeTCM Range Source # | |
Instance detailsDefined in Agda.Interaction.JSONTop |
Pretty TopLevelModuleName Source # | |
Instance detailsDefined in Agda.Syntax.TopLevelModuleName |
HasRange Interval Source # | |
Instance detailsDefined in Agda.Syntax.Position |
HasRange Range Source # | |
Instance detailsDefined in Agda.Syntax.Position |
KillRange Range Source # | |
Instance detailsDefined in Agda.Syntax.Position |
SetRange Range Source # | |
Instance detailsDefined in Agda.Syntax.Position |
FreshName Range Source # | |
Instance detailsDefined in Agda.TypeChecking.Monad.Base |
PrettyTCM Range Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
PrettyTCM TopLevelModuleName Source # | |
Instance detailsDefined in Agda.TypeChecking.Pretty |
EmbPrj Range Source # | Ranges are always deserialised as noRange . |
Instance detailsDefined in Agda.TypeChecking.Serialise.Instances.Common |
EmbPrj TopLevelModuleName Source # | |
Instance detailsDefined in Agda.TypeChecking.Serialise.Instances.Common |
Subst Range Source # | |
Instance detailsDefined in Agda.TypeChecking.Substitute |
Sized TopLevelModuleName Source # | |
Instance detailsDefined in Agda.Syntax.TopLevelModuleName |
Foldable Maybe | |
Instance detailsDefined in Data.Strict.Maybe |
Eq1 Maybe | |
Instance detailsDefined in Data.Strict.Maybe |
Ord1 Maybe | |
Instance detailsDefined in Data.Strict.Maybe |
Read1 Maybe | |
Instance detailsDefined in Data.Strict.Maybe |
Show1 Maybe | |
Instance detailsDefined in Data.Strict.Maybe |
Traversable Maybe | |
Instance detailsDefined in Data.Strict.Maybe |
Applicative Maybe Source # | Note that strict Maybe is an Applicative only modulo strictness.
The laws only hold in the strict semantics.
Eg. pure f * pure _|_ = _|_ , but according to the laws for
Applicative it should be pure (f _|_) .
We ignore this issue here, it applies also to Foldable and Traversable . |
Instance detailsDefined in Agda.Utils.Maybe.Strict |
Functor Maybe | |
Instance detailsDefined in Data.Strict.Maybe |
NFData Interval Source # | |
Instance detailsDefined in Agda.Syntax.Position |
NFData Position Source # | |
Instance detailsDefined in Agda.Syntax.Position |
NFData1 Maybe | |
Instance detailsDefined in Data.Strict.Maybe |
Hashable1 Maybe | |
Instance detailsDefined in Data.Strict.Maybe |
FromJSON1 Maybe | |
Instance detailsDefined in Data.Aeson.Types.FromJSON |
ToJSON Range Source # | |
Instance detailsDefined in Agda.Interaction.JSONTop |
ToJSON1 Maybe | |
Instance detailsDefined in Data.Aeson.Types.ToJSON |
LensClosure MetaInfo Range Source # | |
Instance detailsDefined in Agda.TypeChecking.Monad.Base |
LensClosure MetaVariable Range Source # | |
Instance detailsDefined in Agda.TypeChecking.Monad.Base |
Generic1 Maybe | |
Instance detailsDefined in Data.Strict.Maybe |
Pretty a => Pretty (Interval' (Maybe a)) Source # | |
Instance detailsDefined in Agda.Syntax.Common.Pretty |
Pretty a => Pretty (Position' (Maybe a)) Source # | |
Instance detailsDefined in Agda.Syntax.Common.Pretty |
Pretty a => Pretty (Range' (Maybe a)) Source # | |
Instance detailsDefined in Agda.Syntax.Common.Pretty |
NamesIn a => NamesIn (Maybe a) Source # | |
Instance detailsDefined in Agda.Syntax.Internal.Names |
HasRange (TopLevelModuleName' Range) Source # | |
Instance detailsDefined in Agda.Syntax.Position |
KillRange (TopLevelModuleName' Range) Source # | |
Instance detailsDefined in Agda.Syntax.Position |
KillRange a => KillRange (Maybe a) Source # | |
Instance detailsDefined in Agda.Syntax.Position |
SetRange (TopLevelModuleName' Range) Source # | |
Instance detailsDefined in Agda.Syntax.Position |
Instantiate t => Instantiate (Maybe t) Source # | |
Instance detailsDefined in Agda.TypeChecking.Reduce |
InstantiateFull t => InstantiateFull (Maybe t) Source # | |
Instance detailsDefined in Agda.TypeChecking.Reduce |
Normalise t => Normalise (Maybe t) Source # | |
Instance detailsDefined in Agda.TypeChecking.Reduce |
Simplify t => Simplify (Maybe t) Source # | |
Instance detailsDefined in Agda.TypeChecking.Reduce |
EmbPrj a => EmbPrj (Maybe a) Source # | |
Instance detailsDefined in Agda.TypeChecking.Serialise.Instances.Common |
Apply t => Apply (Maybe t) Source # | |
Instance detailsDefined in Agda.TypeChecking.Substitute |
Null (Maybe a) Source # | |
Instance detailsDefined in Agda.Utils.Maybe.Strict |
Data a => Data (Maybe a) | |
Instance detailsDefined in Data.Strict.Maybe |
Semigroup a => Monoid (Maybe a) | |
Instance detailsDefined in Data.Strict.Maybe |
Semigroup a => Semigroup (Maybe a) | |
Instance detailsDefined in Data.Strict.Maybe |
Generic (Maybe a) | |
Instance detailsDefined in Data.Strict.Maybe |
Read a => Read (Maybe a) | |
Instance detailsDefined in Data.Strict.Maybe |
Show a => Show (Maybe a) | |
Instance detailsDefined in Data.Strict.Maybe |
Binary a => Binary (Maybe a) | |
Instance detailsDefined in Data.Strict.Maybe |
NFData a => NFData (Maybe a) | |
Instance detailsDefined in Data.Strict.Maybe |
Eq a => Eq (Maybe a) | |
Instance detailsDefined in Data.Strict.Maybe |
Ord a => Ord (Maybe a) | |
Instance detailsDefined in Data.Strict.Maybe |
Hashable a => Hashable (Maybe a) | |
Instance detailsDefined in Data.Strict.Maybe |
FromJSON a => FromJSON (Maybe a) | |
Instance detailsDefined in Data.Aeson.Types.FromJSON |
ToJSON a => ToJSON (Maybe a) | |
Instance detailsDefined in Data.Aeson.Types.ToJSON |
Strict (Maybe a) (Maybe a) | |
Instance detailsDefined in Data.Strict.Classes |
FreshName (Range, String) Source # | |
Instance detailsDefined in Agda.TypeChecking.Monad.Base |
type SubstArg Range Source # | |
Instance detailsDefined in Agda.TypeChecking.Substitute |
type Rep1 Maybe | |
Instance detailsDefined in Data.Strict.Maybe |
type Rep (Maybe a) | |
Instance detailsDefined in Data.Strict.Maybe |