[−][src]Module agda_mode::base
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. |
| CompareDirection | An extension of |
| Comparison | |
| ComputeMode | 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. |
| TokenBased | 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. |