| // Copyright (C) 2026 ERRANT DIGITAL INSTITUTE OF TECHNOLOGY (SEIT NGO) % SNAPKITTY COLLECTIVE | |
| // SPDX-License-Identifier: AGPL-3.0-only OR LicenseRef-Commercial | |
| // See LICENSE-AGPL and LICENSE-COMMERCIAL in this repository for license terms. | |
| //! Core term representation for verification-forge's dependent type | |
| //! kernel. | |
| //! | |
| //! This crate is the bottom of the whole verification-forge stack: it | |
| //! depends on nothing else in the workspace, and everything else | |
| //! (`vf-typecheck`'s elaborator, `vf-reducer`'s reduction engine, | |
| //! `vf-kernel`'s trusted checker) is built on the [`Term`]/[`TermId`]/ | |
| //! [`TermArena`] representation defined here. | |
| //! | |
| //! **This crate does not itself decide whether anything is | |
| //! well-typed, well-formed, or true.** It only defines the shape of | |
| //! terms and the structural operations ([`open_at`](TermArena::open_at), | |
| //! [`close_at`](TermArena::close_at), [`shift`](TermArena::shift)) | |
| //! needed to build and take apart binders correctly. See | |
| //! `vf-kernel`'s crate docs and `docs/TRUST_MODEL.md` for where actual | |
| //! typing/proof-checking judgments live. | |
| //! | |
| //! ## Known, documented simplifications (not bugs) | |
| //! | |
| //! - No universe polymorphism: [`Sort`] is `Prop` or `Type(n)` for a | |
| //! concrete `n: u32`, never a universe *variable*. See [`term`]'s | |
| //! module docs. | |
| //! - No proof irrelevance: two [`Term`]s of sort `Prop` that are | |
| //! propositionally equal are not automatically definitionally equal | |
| //! just because they inhabit `Prop`. `vf-kernel`'s `definitional_equal` | |
| //! treats `Prop` exactly like any other sort for this purpose. | |
| //! | |
| //! Both are real restrictions on what can be expressed/proved, listed | |
| //! here (and in `docs/TRUST_MODEL.md`) precisely so nothing downstream | |
| //! can quietly assume more power than this kernel actually has. | |
| pub mod interner; | |
| pub mod term; | |
| pub use interner::{Interner, Symbol}; | |
| pub use term::{ArenaError, Binder, DeBruijnIndex, Sort, Term, TermArena, TermId}; | |