Q package:Agda

The given quantity does not correspond to the expected quantity.

Meta variable for interaction. The InteractionId is usually identical with the metaNumber of MetaInfo. However, if you want to print an interaction meta as just ? instead of ?n, you should set the metaNumber to Nothing while keeping the InteractionId.

Quote an identifier QName.

Quote a term.

Qualified names are non-empty lists of names. Equality on qualified names are just equality on the last name, i.e. the module part is just for show. The SetRange instance for qualified names sets all individual ranges (including those of the module prefix) to the given one.

Something preceeded by a qualified name.

User wrote "@0".

User wrote "@erased".

User wrote nothing.

Origin of Quantity0.

User wrote "@1".

User wrote nothing.

User wrote "@linear".

Origin of Quantity1.

Quantity for linearity. A quantity is a set of natural numbers, indicating possible semantic uses of a variable. A singleton set {n} requires that the corresponding variable is used exactly n times.

Zero uses {0}, erased at runtime.

Linear use {1} (could be updated destructively). Mostly TODO (needs postponable constraints between quantities to compute uses).

Unrestricted use ℕ.

User wrote "@ω".

User wrote nothing.

Origin of Quantityω.