Expand description
Common types (used in both input/output to Agda).
Enums§
- Cohesion
- Cohesion modalities see “Brouwer’s fixed-point theorem in real-cohesive homotopy type theory” (arXiv:1509.07584) types are now given an additional topological layer which the modalities interact with.
- Compare
Direction - An extension of
Comparisonto>=. - Comparison
- Compute
Mode - Modifier for the interactive computation command, specifying the mode of computation and result display.
- Hiding
- Polarity
- Polarity for equality and subtype checking.
- Relevance
- A function argument can be relevant or irrelevant. See “Agda.TypeChecking.Irrelevance”.
- Remove
- Rewrite
- Modifier for interactive commands, specifying the amount of normalization in the output.
- Token
Based - Is the highlighting “token-based”, i.e. based only on information from the lexer?
- UseForce
- Modifier for interactive commands, specifying whether safety checks should be ignored.