logicaffeine_kernel/
lib.rs

1#![cfg_attr(docsrs, feature(doc_cfg))]
2#![doc = include_str!("../README.md")]
3
4mod context;
5#[cfg(feature = "serde")]
6pub mod certificate;
7mod error;
8pub mod inductive_compile;
9pub mod interface;
10pub mod positivity;
11pub mod prelude;
12mod reduction;
13pub mod reify;
14pub mod ring;
15pub mod lia;
16pub mod field_algebra;
17pub mod word_ring;
18pub mod bitvector;
19pub mod cc;
20pub mod eval;
21pub mod simp;
22pub mod elaborate;
23pub mod omega;
24pub mod recheck;
25pub mod recursor;
26pub mod termination;
27mod term;
28mod type_checker;
29
30pub use context::{Context, MutualInductive, StructInfo};
31pub use inductive_compile::{NestedDecl, NestedInfo};
32pub use error::{KernelError, KernelResult};
33pub use eval::{
34    eval_bool, eval_bool_tree, native_compile_bool, native_compile_decide, native_decide,
35};
36pub use reduction::normalize;
37pub use elaborate::{
38    auto_bind_implicits, bind_self_recursion, elaborate, elaborate_app, elaborate_app_against,
39    elaborate_anon_ctor, elaborate_dot, elaborate_in, fill_match_motives, instantiate, resolve_coercion,
40    resolve_instance, surface_elaborate, surface_elaborate_against, unify, unify_in, MetaCtx,
41    ParamKind, ANON_CTOR_MARKER, DOT_MARKER,
42};
43pub use recheck::{double_check, recheck, DoubleCheck, ReCheckError};
44pub use recursor::derive_recursor;
45pub use reify::VarInterner;
46pub use logicaffeine_base::BigInt;
47pub use term::{instantiate_universes, int_lit, lit_bigint, Literal, Term, Universe};
48pub use type_checker::{infer_type, is_subtype};
49
50/// Definitional equality of two terms — exposed for tests that pin conversion
51/// behaviour (structure eta, proof irrelevance) directly.
52pub fn defeq_for_test(ctx: &Context, a: &Term, b: &Term) -> bool {
53    type_checker::def_eq(ctx, a, b)
54}
55
56/// Strict-positivity check of a constructor type — exposed so tests can pin the
57/// paradox fence (negative occurrences rejected, positive functional fields
58/// accepted) directly.
59pub fn check_positivity_for_test(
60    inductive: &str,
61    constructor: &str,
62    ty: &Term,
63) -> KernelResult<()> {
64    positivity::check_positivity(inductive, constructor, ty)
65}
logicaffeine_kernel/lib.rs

logicaffeine_kernel/
lib.rs
