logicaffeine-kernel 0.10.1

Pure Calculus of Constructions type theory - NO LEXICON
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65

#![cfg_attr(docsrs, feature(doc_cfg))]
#![doc = include_str!("../README.md")]

mod context;
#[cfg(feature = "serde")]
pub mod certificate;
mod error;
pub mod inductive_compile;
pub mod interface;
pub mod positivity;
pub mod prelude;
mod reduction;
pub mod reify;
pub mod ring;
pub mod lia;
pub mod field_algebra;
pub mod word_ring;
pub mod bitvector;
pub mod cc;
pub mod eval;
pub mod simp;
pub mod elaborate;
pub mod omega;
pub mod recheck;
pub mod recursor;
pub mod termination;
mod term;
mod type_checker;

pub use context::{Context, MutualInductive, StructInfo};
pub use inductive_compile::{NestedDecl, NestedInfo};
pub use error::{KernelError, KernelResult};
pub use eval::{
    eval_bool, eval_bool_tree, native_compile_bool, native_compile_decide, native_decide,
};
pub use reduction::normalize;
pub use elaborate::{
    auto_bind_implicits, bind_self_recursion, elaborate, elaborate_app, elaborate_app_against,
    elaborate_anon_ctor, elaborate_dot, elaborate_in, fill_match_motives, instantiate, resolve_coercion,
    resolve_instance, surface_elaborate, surface_elaborate_against, unify, unify_in, MetaCtx,
    ParamKind, ANON_CTOR_MARKER, DOT_MARKER,
};
pub use recheck::{double_check, recheck, DoubleCheck, ReCheckError};
pub use recursor::derive_recursor;
pub use reify::VarInterner;
pub use logicaffeine_base::BigInt;
pub use term::{instantiate_universes, int_lit, lit_bigint, Literal, Term, Universe};
pub use type_checker::{infer_type, is_subtype};

/// Definitional equality of two terms — exposed for tests that pin conversion
/// behaviour (structure eta, proof irrelevance) directly.
pub fn defeq_for_test(ctx: &Context, a: &Term, b: &Term) -> bool {
    type_checker::def_eq(ctx, a, b)
}

/// Strict-positivity check of a constructor type — exposed so tests can pin the
/// paradox fence (negative occurrences rejected, positive functional fields
/// accepted) directly.
pub fn check_positivity_for_test(
    inductive: &str,
    constructor: &str,
    ty: &Term,
) -> KernelResult<()> {
    positivity::check_positivity(inductive, constructor, ty)
}