pub fn build_data_structures_env(env: &mut Environment) -> Result<(), String>Expand description
Register all data structure axioms into the given kernel environment.
This adds axioms for the type constructors and core theorems of each data structure. These are axioms rather than definitions because the full inductive definitions would require significantly more kernel infrastructure.