Skip to main content
Module quotient
logicaffeine_
kernel
0.11.0
Module quotient
Module Items
Enums
Functions
In crate logicaffeine_
kernel
logicaffeine_kernel
Module
quotient
Copy item path
Source
Expand description
Certified universe-polymorphic quotient primitives for kernel importers.
Enums
§
Kind
Functions
§
install
Install only a canonical primitive, never an arbitrary trusted input type. The importer separately compares its serialized signature with this one.
signature
The canonical Lean signature, with explicit universe instances throughout.