Primitives

Content created by Fredrik Bakke, Fernando Chu and Egbert Rijke.

Created on 2023-04-27.
Last modified on 2024-09-23.

Modules in the primitives namespace

module primitives where

open import primitives.characters public
open import primitives.floats public
open import primitives.machine-integers public
open import primitives.strings public

Recent changes

• 2024-09-23. Fredrik Bakke. Some typos, wording improvements, and brief prose additions (#1186).
• 2023-05-06. Egbert Rijke. Collecting some easily defined precategories (#598).
• 2023-04-27. Fernando Chu, Fernando Chu, Fernando Chu and Fredrik Bakke. Reflection and solvers (#571).