logicaffeine-kernel 0.10.0

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

[package]
name = "logicaffeine-kernel"
version.workspace = true
edition.workspace = true
authors.workspace = true
repository.workspace = true
homepage.workspace = true
keywords.workspace = true
categories.workspace = true
rust-version.workspace = true
license = "BUSL-1.1"
description = "Pure Calculus of Constructions type theory - NO LEXICON"
readme = "README.md"

[dependencies]
logicaffeine-base = { workspace = true }
# CRITICAL: NO LEXICON DEPENDENCY - Milner Invariant
# Optional serde, off by default so the trusted core stays dependency-free
# unless proof certificates are being (de)serialized.
serde = { version = "1", features = ["derive"], optional = true }

[features]
serde = ["dep:serde"]

# serde_json is dev-only: it powers the example re-checker and the certificate
# tests, but never enters the published library's dependency graph — the trusted
# kernel stays pure.
[dev-dependencies]
serde_json = "1"

# The standalone, independently-auditable proof re-checker. Its only trusted
# inputs are this kernel and a JSON parser. Run with:
#   cargo run -p logicaffeine-kernel --example recheck --features serde -- cert.json
[[example]]
name = "recheck"
required-features = ["serde"]