Two package:Agda

Two :: Three
Agda Agda.Utils.Three
TwoElemArray :: SumEncoding
Agda Agda.Interaction.JSON
A constructor will be encoded to a 2-element array where the first element is the tag of the constructor (modified by the constructorTagModifier) and the second element the encoded contents of the constructor.
_optTwoLevel :: PragmaOptions -> WithDefault 'False
Agda Agda.Interaction.Options Agda.Interaction.Options
lensOptTwoLevel :: Functor f => (WithDefault 'False -> f (WithDefault 'False)) -> PragmaOptions -> f PragmaOptions
Agda Agda.Interaction.Options
optTwoLevel :: PragmaOptions -> Bool
Agda Agda.Interaction.Options
NeedOptionTwoLevel_ :: ErrorName
Agda Agda.Interaction.Options.Errors
BuiltinAgdaLitWord64 :: BuiltinId
Agda Agda.Syntax.Builtin
builtinAgdaLitWord64 :: BuiltinId
Agda Agda.Syntax.Builtin
atLeastTwoParts :: IsExpr e => Parser e Name
Agda Agda.Syntax.Concrete.Operators.Parser
Parses a split-up, unqualified name consisting of at least two name parts. The parser does not check that underscores and other name parts alternate. The range of the resulting name is the range of the first name part that is not an underscore.
LitWord64 :: Word64 -> Literal
Agda Agda.Syntax.Literal
class NotWorse a
Agda Agda.Termination.Order
A partial order, aimed at deciding whether a call graph gets worse during the completion.
notWorse :: NotWorse a => a -> a -> Bool
Agda Agda.Termination.Order
FinalTwoArgumentsNotVisible :: IncorrectTypeForRewriteRelationReason
Agda Agda.TypeChecking.Monad.Base
NeedOptionTwoLevel :: TypeError
Agda Agda.TypeChecking.Monad.Base
ShouldAcceptAtLeastTwoArguments :: IncorrectTypeForRewriteRelationReason
Agda Agda.TypeChecking.Monad.Base
primAgdaLitWord64 :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
Agda Agda.TypeChecking.Monad.Builtin
isTwoLevelEnabled :: HasOptions m => m Bool
Agda Agda.TypeChecking.Monad.Options