Legend
- Boxes
- definitions
- Ellipses
- theorems and lemmas
- Blue border
- the statement of this result is ready to be formalized; all prerequisites are done
- Orange border
- the statement of this result is not ready to be formalized; the blueprint needs more work
- Blue background
- the proof of this result is ready to be formalized; all prerequisites are done
- Green border
- the statement of this result is formalized
- Green background
- the proof of this result is formalized
- Dark green background
- the proof of this result and all its ancestors are formalized
- Dark green border
- this is in Mathlib
Definition
7
Module HeytingLean.Blockchain.Contracts.CLI.PEGDemo.
Lean declarations
- HeytingLean.Blockchain.Contracts.CLI.PEGDemo.readFileE
- HeytingLean.Blockchain.Contracts.CLI.PEGDemo.StepJ
- HeytingLean.Blockchain.Contracts.CLI.PEGDemo.fromJsonE
- HeytingLean.Blockchain.Contracts.CLI.PEGDemo.writeFile
- HeytingLean.Blockchain.Contracts.CLI.PEGDemo.main
- HeytingLean.Blockchain.Contracts.CLI.PEGDemo.main
Definition
10
Module HeytingLean.Blockchain.Rollup.MultiLens.
Lean declarations
- HeytingLean.Blockchain.Rollup.MultiLens.envL
- HeytingLean.Blockchain.Rollup.MultiLens.valueL
- HeytingLean.Blockchain.Rollup.MultiLens.verifyWith
- HeytingLean.Blockchain.Rollup.MultiLens.tensor
- HeytingLean.Blockchain.Rollup.MultiLens.graph
- HeytingLean.Blockchain.Rollup.MultiLens.clifford
- HeytingLean.Blockchain.Rollup.MultiLens.verifyWith_iff_validTransition
- HeytingLean.Blockchain.Rollup.MultiLens.tensor_iff_graph
- HeytingLean.Blockchain.Rollup.MultiLens.tensor_iff_clifford
- HeytingLean.Blockchain.Rollup.MultiLens.graph_iff_clifford
Definition
11
Module HeytingLean.Blockchain.Rollup.StateTransition.
Lean declarations
- HeytingLean.Blockchain.Rollup.StateTransition.Spec
- HeytingLean.Blockchain.Rollup.StateTransition.validTransition
- HeytingLean.Blockchain.Rollup.StateTransition.program
- HeytingLean.Blockchain.Rollup.StateTransition.occamEval
- HeytingLean.Blockchain.Rollup.StateTransition.occamEval_eq_eval
- HeytingLean.Blockchain.Rollup.StateTransition.toy
- HeytingLean.Blockchain.Rollup.StateTransition.counter
Definition
12
Module HeytingLean.Bridges.Clifford.
Lean declarations
- HeytingLean.Bridges.Clifford.Pair
- HeytingLean.Bridges.Clifford.Model
- HeytingLean.Bridges.Clifford.Carrier
- HeytingLean.Bridges.Clifford.project_idem
- HeytingLean.Bridges.Clifford.encode_eulerBoundary_fst
- HeytingLean.Bridges.Clifford.encode_eulerBoundary_snd
- HeytingLean.Bridges.Clifford.stageEffectCompatible
Definition
14
Module HeytingLean.Bridges.Clifford.Projector.
Lean declarations
- HeytingLean.Bridges.Clifford.Projector.Carrier
- HeytingLean.Bridges.Clifford.Projector.Model
- HeytingLean.Bridges.Clifford.Projector.Carrier
- HeytingLean.Bridges.Clifford.Projector.toPair
- HeytingLean.Bridges.Clifford.Projector.fromPair
- HeytingLean.Bridges.Clifford.Projector.stageEffectCompatible
- HeytingLean.Bridges.Clifford.Projector.projected
- HeytingLean.Bridges.Clifford.Projector.Invariants
- HeytingLean.Bridges.Clifford.Projector.invariants
Definition
17
Module HeytingLean.Bridges.Graph.
Lean declarations
- HeytingLean.Bridges.Graph.Model
- HeytingLean.Bridges.Graph.adjacency
- HeytingLean.Bridges.Graph.Carrier
- HeytingLean.Bridges.Graph.encode_eulerBoundary
- HeytingLean.Bridges.Graph.adjacency_refl
- HeytingLean.Bridges.Graph.adjacency_trans
- HeytingLean.Bridges.Graph.adjacency_mono_left
- HeytingLean.Bridges.Graph.adjacency_mono_right
- HeytingLean.Bridges.Graph.stageEffectCompatible
Definition
18
Module HeytingLean.Bridges.Graph.Alexandroff.
Lean declarations
- HeytingLean.Bridges.Graph.Alexandroff.Model
- HeytingLean.Bridges.Graph.Alexandroff.Carrier
- HeytingLean.Bridges.Graph.Alexandroff.memOpen
- HeytingLean.Bridges.Graph.Alexandroff.mem_of_le
- HeytingLean.Bridges.Graph.Alexandroff.mem_inf
- HeytingLean.Bridges.Graph.Alexandroff.mem_sup_project
- HeytingLean.Bridges.Graph.Alexandroff.mem_stageCollapseAt
- HeytingLean.Bridges.Graph.Alexandroff.mem_stageExpandAt
- HeytingLean.Bridges.Graph.Alexandroff.mem_stageOccam
- HeytingLean.Bridges.Graph.Alexandroff.stageEffectCompatible
Definition
20
Module HeytingLean.Bridges.Tensor.
Lean declarations
- HeytingLean.Bridges.Tensor.Point
- HeytingLean.Bridges.Tensor.Model
- HeytingLean.Bridges.Tensor.Carrier
- HeytingLean.Bridges.Tensor.interpret_idem
- HeytingLean.Bridges.Tensor.eulerBoundary_vector
- HeytingLean.Bridges.Tensor.pointwiseMin
- HeytingLean.Bridges.Tensor.pointwiseMax
- HeytingLean.Bridges.Tensor.stageEffectCompatible
Definition
21
Module HeytingLean.Bridges.Tensor.Intensity.
Lean declarations
- HeytingLean.Bridges.Tensor.Intensity.Bounds
- HeytingLean.Bridges.Tensor.Intensity.Profile
- HeytingLean.Bridges.Tensor.Intensity.ofPoint
- HeytingLean.Bridges.Tensor.Intensity.asPoint
- HeytingLean.Bridges.Tensor.Intensity.Model
- HeytingLean.Bridges.Tensor.Intensity.intensityPoint
- HeytingLean.Bridges.Tensor.Intensity.Carrier
- HeytingLean.Bridges.Tensor.Intensity.toPoint
- HeytingLean.Bridges.Tensor.Intensity.stageEffectCompatible
Definition
35
Module HeytingLean.CLI.LoFCanonExample.
Lean declarations
- HeytingLean.CLI.LoFCanonExample.canonicalize
- HeytingLean.CLI.LoFCanonExample.demoHash
- HeytingLean.CLI.LoFCanonExample.LensCommitments
- HeytingLean.CLI.LoFCanonExample.computeLensCommitmentsIO
- HeytingLean.CLI.LoFCanonExample.decodeTensorToCanonical
- HeytingLean.CLI.LoFCanonExample.decodeGraphToCanonical
- HeytingLean.CLI.LoFCanonExample.decodeCliffordToCanonical
- HeytingLean.CLI.LoFCanonExample.mkSampleForm
- HeytingLean.CLI.LoFCanonExample.Output
- HeytingLean.CLI.LoFCanonExample.outputToJson
- HeytingLean.CLI.LoFCanonExample.readFileIfExists
- HeytingLean.CLI.LoFCanonExample.parseFormJson
Definition
36
Module HeytingLean.CLI.SurrealPGNorm.
Lean declarations
- HeytingLean.CLI.SurrealPGNorm.stabilizeStep
- HeytingLean.CLI.SurrealPGNorm.stabilizeK
- HeytingLean.CLI.SurrealPGNorm.zero
- HeytingLean.CLI.SurrealPGNorm.one
- HeytingLean.CLI.SurrealPGNorm.negOne
- HeytingLean.CLI.SurrealPGNorm.Args
- HeytingLean.CLI.SurrealPGNorm.parseArgs
- HeytingLean.CLI.SurrealPGNorm.describe
- HeytingLean.CLI.SurrealPGNorm.runDemoText
- HeytingLean.CLI.SurrealPGNorm.jsonEscape
- HeytingLean.CLI.SurrealPGNorm.runDemoJson
- HeytingLean.CLI.SurrealPGNorm.SurrealPGNorm.main
Definition
41
Module HeytingLean.Computing.CircuitClassic.
Lean declarations
- HeytingLean.Computing.CircuitClassic.Gate
- HeytingLean.Computing.CircuitClassic.Port
- HeytingLean.Computing.CircuitClassic.Circuit
- HeytingLean.Computing.CircuitClassic.normalize
- HeytingLean.Computing.CircuitClassic.normalize_idem
- HeytingLean.Computing.CircuitClassic.depth
- HeytingLean.Computing.CircuitClassic.depth_normalize_le
- HeytingLean.Computing.CircuitClassic.occamByDepth
- HeytingLean.Computing.CircuitClassic.occamByDepth_idem
- HeytingLean.Computing.CircuitClassic.synthPar
- HeytingLean.Computing.CircuitClassic.synthSeq
- HeytingLean.Computing.CircuitClassic.gate
Definition
42
Module HeytingLean.Contracts.Examples.
Lean declarations
- HeytingLean.Contracts.Examples.identity
- HeytingLean.Contracts.Examples.tensor
- HeytingLean.Contracts.Examples.graph
- HeytingLean.Contracts.Examples.clifford
- HeytingLean.Contracts.Examples.BridgeFlags
- HeytingLean.Contracts.Examples.BridgeFlags.legacy
- HeytingLean.Contracts.Examples.BridgeFlags.runtime
- HeytingLean.Contracts.Examples.BridgeFlags.default
- HeytingLean.Contracts.Examples.alexandroffFlags
- HeytingLean.Contracts.Examples.intensityFlags
- HeytingLean.Contracts.Examples.BridgePack
- HeytingLean.Contracts.Examples.BridgeSuite
Definition
45
Module HeytingLean.Crypto.AlgRegistry.
Lean declarations
- HeytingLean.Crypto.AlgRegistry.AlgId
- HeytingLean.Crypto.AlgRegistry.Diamond
- HeytingLean.Crypto.AlgRegistry.Entry
- HeytingLean.Crypto.AlgRegistry.Rotation
- HeytingLean.Crypto.AlgRegistry.accepts
- HeytingLean.Crypto.AlgRegistry.WellFormed
- HeytingLean.Crypto.AlgRegistry.before_iff_old
- HeytingLean.Crypto.AlgRegistry.during_iff_old_or_new
- HeytingLean.Crypto.AlgRegistry.after_iff_new
- HeytingLean.Crypto.AlgRegistry.ReceiptView
- HeytingLean.Crypto.AlgRegistry.valid
- HeytingLean.Crypto.AlgRegistry.meaning_over_mechanism
Definition
46
Module HeytingLean.Crypto.BoolLens.
Lean declarations
- HeytingLean.Crypto.BoolLens.Env
- HeytingLean.Crypto.BoolLens.eval
- HeytingLean.Crypto.BoolLens.Stack
- HeytingLean.Crypto.BoolLens.Trace
- HeytingLean.Crypto.BoolLens.step
- HeytingLean.Crypto.BoolLens.exec
- HeytingLean.Crypto.BoolLens.traceFrom
- HeytingLean.Crypto.BoolLens.run
- HeytingLean.Crypto.BoolLens.exec_append
- HeytingLean.Crypto.BoolLens.traceFrom_cons_head
- HeytingLean.Crypto.BoolLens.run_compile_value
- HeytingLean.Crypto.BoolLens.canonicalTrace
Definition
48
Module HeytingLean.Crypto.Commit.NucleusCommit.
Lean declarations
- HeytingLean.Crypto.Commit.NucleusCommit.EncodableWitness
- HeytingLean.Crypto.Commit.NucleusCommit.NucleusCtx
- HeytingLean.Crypto.Commit.NucleusCommit.commit
- HeytingLean.Crypto.Commit.NucleusCommit.preimage
- HeytingLean.Crypto.Commit.NucleusCommit.equivR
- HeytingLean.Crypto.Commit.NucleusCommit.equivR_refl
- HeytingLean.Crypto.Commit.NucleusCommit.equivR_symm
- HeytingLean.Crypto.Commit.NucleusCommit.equivR_trans
- HeytingLean.Crypto.Commit.NucleusCommit.QuotR
- HeytingLean.Crypto.Commit.NucleusCommit.quotToStmt
- HeytingLean.Crypto.Commit.NucleusCommit.Rel
- HeytingLean.Crypto.Commit.NucleusCommit.Rel_functional
Definition
51
Module HeytingLean.Crypto.CoreTypes.
Lean declarations
- HeytingLean.Crypto.CoreTypes.EvalOp
- HeytingLean.Crypto.CoreTypes.ofString
- HeytingLean.Crypto.CoreTypes.EvalStepCore
- HeytingLean.Crypto.CoreTypes.WitnessCore
- HeytingLean.Crypto.CoreTypes.PublicInputsCore
- HeytingLean.Crypto.CoreTypes.PublicInputsCore.isValid
- HeytingLean.Crypto.CoreTypes.WitnessCore.isSane
- HeytingLean.Crypto.CoreTypes.toCorePublic
- HeytingLean.Crypto.CoreTypes.toCoreWitness
Definition
56
Module HeytingLean.Crypto.Hash.Poseidon.
Lean declarations
- HeytingLean.Crypto.Hash.Poseidon.poseidonCommit
- HeytingLean.Crypto.Hash.Poseidon.commitForm
- HeytingLean.Crypto.Hash.Poseidon.commitTensor
- HeytingLean.Crypto.Hash.Poseidon.commitGraph
- HeytingLean.Crypto.Hash.Poseidon.commitClifford
- HeytingLean.Crypto.Hash.Poseidon.commitFormIO
- HeytingLean.Crypto.Hash.Poseidon.commitTensorIO
- HeytingLean.Crypto.Hash.Poseidon.commitGraphIO
- HeytingLean.Crypto.Hash.Poseidon.commitCliffordIO
Definition
57
Module HeytingLean.Crypto.Lattice.Stages.
Lean declarations
- HeytingLean.Crypto.Lattice.Stages.ctMeet
- HeytingLean.Crypto.Lattice.Stages.ctJoin
- HeytingLean.Crypto.Lattice.Stages.ctImp
- HeytingLean.Crypto.Lattice.Stages.ctJoin_mono_left
- HeytingLean.Crypto.Lattice.Stages.ctJoin_mono_right
- HeytingLean.Crypto.Lattice.Stages.ctMeet_mono_left
- HeytingLean.Crypto.Lattice.Stages.ctMeet_mono_right
- HeytingLean.Crypto.Lattice.Stages.ctImp_mono_right
- HeytingLean.Crypto.Lattice.Stages.Ops
- HeytingLean.Crypto.Lattice.Stages.opsAtBoolean
- HeytingLean.Crypto.Lattice.Stages.opsAtOrthomodular
- HeytingLean.Crypto.Lattice.Stages.fast_reduce
Definition
70
Module HeytingLean.Crypto.ZK.Backends.Air.
Lean declarations
- HeytingLean.Crypto.ZK.Backends.Air.AirSys
- HeytingLean.Crypto.ZK.Backends.Air.AirAssign
- HeytingLean.Crypto.ZK.Backends.Air.airCompile
- HeytingLean.Crypto.ZK.Backends.Air.airSatisfies
- HeytingLean.Crypto.ZK.Backends.Air.airPublic
- HeytingLean.Crypto.ZK.Backends.Air.AirBackend
- HeytingLean.Crypto.ZK.Backends.Air.air_sound
- HeytingLean.Crypto.ZK.Backends.Air.air_complete
Definition
71
Module HeytingLean.Crypto.ZK.Backends.Bullet.
Lean declarations
- HeytingLean.Crypto.ZK.Backends.Bullet.BulletSys
- HeytingLean.Crypto.ZK.Backends.Bullet.BulletAssign
- HeytingLean.Crypto.ZK.Backends.Bullet.bulletCompile
- HeytingLean.Crypto.ZK.Backends.Bullet.bulletSatisfies
- HeytingLean.Crypto.ZK.Backends.Bullet.bulletPublic
- HeytingLean.Crypto.ZK.Backends.Bullet.BulletBackend
- HeytingLean.Crypto.ZK.Backends.Bullet.bullet_sound
- HeytingLean.Crypto.ZK.Backends.Bullet.bullet_complete
Definition
72
Module HeytingLean.Crypto.ZK.Backends.Plonk.
Lean declarations
- HeytingLean.Crypto.ZK.Backends.Plonk.PlonkSys
- HeytingLean.Crypto.ZK.Backends.Plonk.PlonkAssign
- HeytingLean.Crypto.ZK.Backends.Plonk.plonkCompile
- HeytingLean.Crypto.ZK.Backends.Plonk.plonkSatisfies
- HeytingLean.Crypto.ZK.Backends.Plonk.plonkPublic
- HeytingLean.Crypto.ZK.Backends.Plonk.PlonkBackend
- HeytingLean.Crypto.ZK.Backends.Plonk.plonk_sound
- HeytingLean.Crypto.ZK.Backends.Plonk.plonk_complete
Definition
85
Module HeytingLean.Crypto.ZK.Export.
Lean declarations
- HeytingLean.Crypto.ZK.Export.linCombToJson
- HeytingLean.Crypto.ZK.Export.constraintToJson
- HeytingLean.Crypto.ZK.Export.systemToJson
- HeytingLean.Crypto.ZK.Export.assignmentToJson
- HeytingLean.Crypto.ZK.Export.compiledToJson
- HeytingLean.Crypto.ZK.Export.jsonToLinComb
- HeytingLean.Crypto.ZK.Export.jsonToConstraint
- HeytingLean.Crypto.ZK.Export.jsonToSystem
- HeytingLean.Crypto.ZK.Export.jsonToAssignment
- HeytingLean.Crypto.ZK.Export.assignmentOfArray
- HeytingLean.Crypto.ZK.Export.linCombToJson
- HeytingLean.Crypto.ZK.Export.airSystemToJson
Definition
88
Module HeytingLean.Crypto.ZK.LensProofs.
Lean declarations
- HeytingLean.Crypto.ZK.LensProofs.ProofCore
- HeytingLean.Crypto.ZK.LensProofs.ProofWith
- HeytingLean.Crypto.ZK.LensProofs.ofCore
- HeytingLean.Crypto.ZK.LensProofs.verifyWith
- HeytingLean.Crypto.ZK.LensProofs.holdsCore
- HeytingLean.Crypto.ZK.LensProofs.verifyWith_iff_holdsCore
- HeytingLean.Crypto.ZK.LensProofs.verifyWith_ofCore
- HeytingLean.Crypto.ZK.LensProofs.verifyTensor
- HeytingLean.Crypto.ZK.LensProofs.verifyGraph
- HeytingLean.Crypto.ZK.LensProofs.verifyClifford
- HeytingLean.Crypto.ZK.LensProofs.tensor_iff_graph
- HeytingLean.Crypto.ZK.LensProofs.tensor_iff_clifford
Definition
89
Module HeytingLean.Crypto.ZK.PlonkIR.
Lean declarations
- HeytingLean.Crypto.ZK.PlonkIR.LinComb
- HeytingLean.Crypto.ZK.PlonkIR.Gate
- HeytingLean.Crypto.ZK.PlonkIR.System
- HeytingLean.Crypto.ZK.PlonkIR.eqVarConstraint
- HeytingLean.Crypto.ZK.PlonkIR.copyPairs
- HeytingLean.Crypto.ZK.PlonkIR.copyConstraintSystem
- HeytingLean.Crypto.ZK.PlonkIR.System.toR1CS
- HeytingLean.Crypto.ZK.PlonkIR.System.satisfiedNative
- HeytingLean.Crypto.ZK.PlonkIR.eqVarConstraint_refl_satisfied
- HeytingLean.Crypto.ZK.PlonkIR.copySatisfied_of_pairs
- HeytingLean.Crypto.ZK.PlonkIR.satisfiedNative_iff_r1cs_of_pairs
- HeytingLean.Crypto.ZK.PlonkIR.copySatisfied_of_pairs
Definition
90
Module HeytingLean.Crypto.ZK.R1CS.
Lean declarations
- HeytingLean.Crypto.ZK.R1CS.Var
- HeytingLean.Crypto.ZK.R1CS.LinComb
- HeytingLean.Crypto.ZK.R1CS.eval
- HeytingLean.Crypto.ZK.R1CS.ofConst
- HeytingLean.Crypto.ZK.R1CS.single
- HeytingLean.Crypto.ZK.R1CS.Constraint
- HeytingLean.Crypto.ZK.R1CS.Constraint.satisfied
- HeytingLean.Crypto.ZK.R1CS.System
- HeytingLean.Crypto.ZK.R1CS.System.satisfied
Definition
91
Module HeytingLean.Crypto.ZK.R1CSBool.
Lean declarations
- HeytingLean.Crypto.ZK.R1CSBool.Builder
- HeytingLean.Crypto.ZK.R1CSBool.fresh
- HeytingLean.Crypto.ZK.R1CSBool.addConstraint
- HeytingLean.Crypto.ZK.R1CSBool.boolConstraint
- HeytingLean.Crypto.ZK.R1CSBool.eqConstConstraint
- HeytingLean.Crypto.ZK.R1CSBool.eqConstConstraint_head_satisfied
- HeytingLean.Crypto.ZK.R1CSBool.eqConstraint
- HeytingLean.Crypto.ZK.R1CSBool.Compiled
- HeytingLean.Crypto.ZK.R1CSBool.Matches
- HeytingLean.Crypto.ZK.R1CSBool.Bounded
- HeytingLean.Crypto.ZK.R1CSBool.Builder.system
- HeytingLean.Crypto.ZK.R1CSBool.SupportOK
Definition
94
Module HeytingLean.Crypto.ZK.Support.
Lean declarations
- HeytingLean.Crypto.ZK.Support.AgreesOn
- HeytingLean.Crypto.ZK.Support.symm
- HeytingLean.Crypto.ZK.Support.trans
- HeytingLean.Crypto.ZK.Support.mono
- HeytingLean.Crypto.ZK.Support.insert
- HeytingLean.Crypto.ZK.Support.erase
- HeytingLean.Crypto.ZK.Support.support
- HeytingLean.Crypto.ZK.Support.support_terms_mem
- HeytingLean.Crypto.ZK.Support.agree_on_term
- HeytingLean.Crypto.ZK.Support.support_tail
- HeytingLean.Crypto.ZK.Support.eval_ext
- HeytingLean.Crypto.ZK.Support.support
Definition
95
Module HeytingLean.Epistemic.Occam.
Lean declarations
- HeytingLean.Epistemic.Occam.breathe
- HeytingLean.Epistemic.Occam.birth_spec
- HeytingLean.Epistemic.Occam.birth_min
- HeytingLean.Epistemic.Occam.birth_le_one
- HeytingLean.Epistemic.Occam.birth_eq_zero_iff
- HeytingLean.Epistemic.Occam.fixed_of_birth_zero
- HeytingLean.Epistemic.Occam.occamCandidates
- HeytingLean.Epistemic.Occam.occamCandidate_le
- HeytingLean.Epistemic.Occam.occamCandidate_fixed
- HeytingLean.Epistemic.Occam.occamBirth_spec
- HeytingLean.Epistemic.Occam.occamBirth_min
- HeytingLean.Epistemic.Occam.occamBirth_zero
Definition
101
Module HeytingLean.LoF.ComparisonNucleus.RTTRI.
Lean declarations
- HeytingLean.LoF.ComparisonNucleus.RTTRI.enc
- HeytingLean.LoF.ComparisonNucleus.RTTRI.dec
- HeytingLean.LoF.ComparisonNucleus.RTTRI.R
- HeytingLean.LoF.ComparisonNucleus.RTTRI.sup
- HeytingLean.LoF.ComparisonNucleus.RTTRI.supR
- HeytingLean.LoF.ComparisonNucleus.RTTRI.enc_supR_le
- HeytingLean.LoF.ComparisonNucleus.RTTRI.HeytingMorphHyp
- HeytingLean.LoF.ComparisonNucleus.RTTRI.neg
- HeytingLean.LoF.ComparisonNucleus.RTTRI.negR
- HeytingLean.LoF.ComparisonNucleus.RTTRI.imp
- HeytingLean.LoF.ComparisonNucleus.RTTRI.impR
Definition
102
Module HeytingLean.LoF.ComparisonNucleus.Soundness.
Lean declarations
- HeytingLean.LoF.ComparisonNucleus.Soundness.act_monotone
- HeytingLean.LoF.ComparisonNucleus.Soundness.act_le
- HeytingLean.LoF.ComparisonNucleus.Soundness.act_idem_le
- HeytingLean.LoF.ComparisonNucleus.Soundness.nucleusOfGcMeet
- HeytingLean.LoF.ComparisonNucleus.Soundness.frobenius_map_inf
- HeytingLean.LoF.ComparisonNucleus.Soundness.nucleusOfGcFrobenius
- HeytingLean.LoF.ComparisonNucleus.Soundness.HypPack
- HeytingLean.LoF.ComparisonNucleus.Soundness.spec
- HeytingLean.LoF.ComparisonNucleus.Soundness.nucleus
- HeytingLean.LoF.ComparisonNucleus.Soundness.nucleus_apply
- HeytingLean.LoF.ComparisonNucleus.Soundness.act_coe_
Definition
112
Module HeytingLean.LoF.Nucleus.
Lean declarations
- HeytingLean.LoF.Nucleus.Reentry
- HeytingLean.LoF.Nucleus.map_sup
- HeytingLean.LoF.Nucleus.map_sup_le
- HeytingLean.LoF.Nucleus.map_himp_le
- HeytingLean.LoF.Nucleus.Omega
- HeytingLean.LoF.Nucleus.primordial_le_of_fixed
- HeytingLean.LoF.Nucleus.mk
- HeytingLean.LoF.Nucleus.process
- HeytingLean.LoF.Nucleus.counterProcess
- HeytingLean.LoF.Nucleus.process_le_of_pos
- HeytingLean.LoF.Nucleus.process_inf_counter
- HeytingLean.LoF.Nucleus.process_pos
Definition
118
Module HeytingLean.Logic.Dialectic.
Lean declarations
- HeytingLean.Logic.Dialectic.synth
- HeytingLean.Logic.Dialectic.le_synth_left
- HeytingLean.Logic.Dialectic.le_synth_right
- HeytingLean.Logic.Dialectic.synth_le
- HeytingLean.Logic.Dialectic.pole_left_to_synthesis
- HeytingLean.Logic.Dialectic.pole_right_to_synthesis
- HeytingLean.Logic.Dialectic.synthesis_least
- HeytingLean.Logic.Dialectic.synthOmega
- HeytingLean.Logic.Dialectic.synthOmega_le
- HeytingLean.Logic.Dialectic.oscillationOmega
- HeytingLean.Logic.Dialectic.le_synthOmega_left
- HeytingLean.Logic.Dialectic.le_synthOmega_right
Definition
119
Module HeytingLean.Logic.ModalDial.
Lean declarations
- HeytingLean.Logic.ModalDial.Dial
- HeytingLean.Logic.ModalDial.collapse
- HeytingLean.Logic.ModalDial.expand
- HeytingLean.Logic.ModalDial.collapse_monotone
- HeytingLean.Logic.ModalDial.expand_monotone
- HeytingLean.Logic.ModalDial.collapse_le_next
- HeytingLean.Logic.ModalDial.box_le_collapse
- HeytingLean.Logic.ModalDial.box_le_expand
- HeytingLean.Logic.ModalDial.DialParam
- HeytingLean.Logic.ModalDial.collapse
- HeytingLean.Logic.ModalDial.expand
- HeytingLean.Logic.ModalDial.collapse_monotone
Definition
120
Module HeytingLean.Logic.PSR.
Lean declarations
- HeytingLean.Logic.PSR.Sufficient
- HeytingLean.Logic.PSR.sufficient_of_fixed
- HeytingLean.Logic.PSR.fixed_of_sufficient
- HeytingLean.Logic.PSR.Step
- HeytingLean.Logic.PSR.reachable
- HeytingLean.Logic.PSR.reachable_step
- HeytingLean.Logic.PSR.reachable_trans
- HeytingLean.Logic.PSR.reachable_of_breathe
- HeytingLean.Logic.PSR.reachable_iff_exists_breathe
- HeytingLean.Logic.PSR.breathe_le_of_sufficient
- HeytingLean.Logic.PSR.sufficient_reachable
- HeytingLean.Logic.PSR.sufficient_stable
Definition
121
Module HeytingLean.Logic.ResiduatedLadder.
Lean declarations
- HeytingLean.Logic.ResiduatedLadder.deduction
- HeytingLean.Logic.ResiduatedLadder.abduction
- HeytingLean.Logic.ResiduatedLadder.induction
- HeytingLean.Logic.ResiduatedLadder.deduction_iff_induction
- HeytingLean.Logic.ResiduatedLadder.deduction_iff_abduction
- HeytingLean.Logic.ResiduatedLadder.abduction_iff_induction
- HeytingLean.Logic.ResiduatedLadder.induction_le_from_euler
- HeytingLean.Logic.ResiduatedLadder.eulerBoundary_collapse
- HeytingLean.Logic.ResiduatedLadder.eulerBoundary_induction_collapse
- HeytingLean.Logic.ResiduatedLadder.eulerBoundary_abduction_collapse
- HeytingLean.Logic.ResiduatedLadder.himp_closed
- HeytingLean.Logic.ResiduatedLadder.map_himp_le
Definition
122
Module HeytingLean.Logic.StageSemantics.
Lean declarations
- HeytingLean.Logic.StageSemantics.MvCore
- HeytingLean.Logic.StageSemantics.EffectCore
- HeytingLean.Logic.StageSemantics.OmlCore
- HeytingLean.Logic.StageSemantics.effectCompatible
- HeytingLean.Logic.StageSemantics.effectCompatible_orthocomplement
- HeytingLean.Logic.StageSemantics.map_himp_le
- HeytingLean.Logic.StageSemantics.collapseAtOmega_monotone
- HeytingLean.Logic.StageSemantics.expandAtOmega_monotone
- HeytingLean.Logic.StageSemantics.Bridge
- HeytingLean.Logic.StageSemantics.stageMvAdd
- HeytingLean.Logic.StageSemantics.stageMvNeg
- HeytingLean.Logic.StageSemantics.stageMvZero
Definition
123
Module HeytingLean.Logic.Trace.
Lean declarations
- HeytingLean.Logic.Trace.Independence
- HeytingLean.Logic.Trace.Word
- HeytingLean.Logic.Trace.Step
- HeytingLean.Logic.Trace.Congruence
- HeytingLean.Logic.Trace.congr_symm
- HeytingLean.Logic.Trace.congr_trans
- HeytingLean.Logic.Trace.TraceMonoid
- HeytingLean.Logic.Trace.mk
- HeytingLean.Logic.Trace.empty
- HeytingLean.Logic.Trace.mul
- HeytingLean.Logic.Trace.of
- HeytingLean.Logic.Trace.ConcurrencySystem
Definition
128
Module HeytingLean.Noneism.Semantics.LP.
Lean declarations
- HeytingLean.Noneism.Semantics.LP.TV
- HeytingLean.Noneism.Semantics.LP.designated
- HeytingLean.Noneism.Semantics.LP.not
- HeytingLean.Noneism.Semantics.LP.and
- HeytingLean.Noneism.Semantics.LP.or
- HeytingLean.Noneism.Semantics.LP.imp
- HeytingLean.Noneism.Semantics.LP.Env
- HeytingLean.Noneism.Semantics.LP.eval
- HeytingLean.Noneism.Semantics.LP.Holds
- HeytingLean.Noneism.Semantics.LP.Entails
- HeytingLean.Noneism.Semantics.LP.Atom
- HeytingLean.Noneism.Semantics.LP.counterEnv
Definition
129
Module HeytingLean.Noneism.Semantics.ModalPriest.
Lean declarations
- HeytingLean.Noneism.Semantics.ModalPriest.Kind
- HeytingLean.Noneism.Semantics.ModalPriest.Model
- HeytingLean.Noneism.Semantics.ModalPriest.cp_holdsTrue
- HeytingLean.Noneism.Semantics.ModalPriest.Valuation
- HeytingLean.Noneism.Semantics.ModalPriest.update
- HeytingLean.Noneism.Semantics.ModalPriest.evalTerm
- HeytingLean.Noneism.Semantics.ModalPriest.eval
Definition
131
Module HeytingLean.Noneism.Semantics.Sylvan.
Lean declarations
- HeytingLean.Noneism.Semantics.Sylvan.Model
- HeytingLean.Noneism.Semantics.Sylvan.Valuation
- HeytingLean.Noneism.Semantics.Sylvan.update
- HeytingLean.Noneism.Semantics.Sylvan.update_self
- HeytingLean.Noneism.Semantics.Sylvan.update_other
- HeytingLean.Noneism.Semantics.Sylvan.evalTerm
- HeytingLean.Noneism.Semantics.Sylvan.eval
- HeytingLean.Noneism.Semantics.Sylvan.ui_pi
- HeytingLean.Noneism.Semantics.Sylvan.eg_sigma
Definition
135
Module HeytingLean.Noneism.Tests.ModalPriest.
Lean declarations
- HeytingLean.Noneism.Tests.ModalPriest.Atom
- HeytingLean.Noneism.Tests.ModalPriest.W
- HeytingLean.Noneism.Tests.ModalPriest.kind
- HeytingLean.Noneism.Tests.ModalPriest.D
- HeytingLean.Noneism.Tests.ModalPriest.holmes
- HeytingLean.Noneism.Tests.ModalPriest.interp
- HeytingLean.Noneism.Tests.ModalPriest.existsP
- HeytingLean.Noneism.Tests.ModalPriest.about
- HeytingLean.Noneism.Tests.ModalPriest.realize
- HeytingLean.Noneism.Tests.ModalPriest.item
- HeytingLean.Noneism.Tests.ModalPriest.M
- HeytingLean.Noneism.Tests.ModalPriest.cp_holds_on_realization
Definition
136
Module HeytingLean.Noneism.Tests.Paraconsistent.
Lean declarations
- HeytingLean.Noneism.Tests.Paraconsistent.Atom
- HeytingLean.Noneism.Tests.Paraconsistent.W
- HeytingLean.Noneism.Tests.Paraconsistent.w0
- HeytingLean.Noneism.Tests.Paraconsistent.frame
- HeytingLean.Noneism.Tests.Paraconsistent.D
- HeytingLean.Noneism.Tests.Paraconsistent.interp
- HeytingLean.Noneism.Tests.Paraconsistent.existsP
- HeytingLean.Noneism.Tests.Paraconsistent.M
- HeytingLean.Noneism.Tests.Paraconsistent.A
- HeytingLean.Noneism.Tests.Paraconsistent.B
- HeytingLean.Noneism.Tests.Paraconsistent.A_true_at_w0
- HeytingLean.Noneism.Tests.Paraconsistent.notA_true_at_w0
Definition
142
Module HeytingLean.Numbers.Surreal.ComparisonDefault.
Lean declarations
- HeytingLean.Numbers.Surreal.ComparisonDefault.R_core
- HeytingLean.Numbers.Surreal.ComparisonDefault.f_id
- HeytingLean.Numbers.Surreal.ComparisonDefault.g_id
- HeytingLean.Numbers.Surreal.ComparisonDefault.fixed_coe
- HeytingLean.Numbers.Surreal.ComparisonDefault.gc_id
- HeytingLean.Numbers.Surreal.ComparisonDefault.comparison_is_identity
- HeytingLean.Numbers.Surreal.ComparisonDefault.factor
- HeytingLean.Numbers.Surreal.ComparisonDefault.factor_commutes
- HeytingLean.Numbers.Surreal.ComparisonDefault.factor_unique
- HeytingLean.Numbers.Surreal.ComparisonDefault.kernel_nucleus_id
Definition
143
Module HeytingLean.Numbers.Surreal.ComparisonLoF.
Lean declarations
- HeytingLean.Numbers.Surreal.ComparisonLoF.RL_default
- HeytingLean.Numbers.Surreal.ComparisonLoF.f_lof
- HeytingLean.Numbers.Surreal.ComparisonLoF.g_lof
- HeytingLean.Numbers.Surreal.ComparisonLoF.gc_lof
- HeytingLean.Numbers.Surreal.ComparisonLoF.R_comp_lof
- HeytingLean.Numbers.Surreal.ComparisonLoF.factor_lof
- HeytingLean.Numbers.Surreal.ComparisonLoF.diamond_commutes_pointwise_le
- HeytingLean.Numbers.Surreal.ComparisonLoF.compSpec_lof
- HeytingLean.Numbers.Surreal.ComparisonLoF.strong_lof
- HeytingLean.Numbers.Surreal.ComparisonLoF.nucleus_comparison_lof
Definition
146
Module HeytingLean.Numbers.Surreal.GameN.
Lean declarations
- HeytingLean.Numbers.Surreal.GameN.GameN
- HeytingLean.Numbers.Surreal.GameN.Game
- HeytingLean.Numbers.Surreal.GameN.day
- HeytingLean.Numbers.Surreal.GameN.L
- HeytingLean.Numbers.Surreal.GameN.R
- HeytingLean.Numbers.Surreal.GameN.mem_L_day_le
- HeytingLean.Numbers.Surreal.GameN.mem_R_day_le
- HeytingLean.Numbers.Surreal.GameN.mem_L_day_lt
- HeytingLean.Numbers.Surreal.GameN.mem_R_day_lt
Definition
149
Module HeytingLean.Numbers.Surreal.Normalized.
Lean declarations
- HeytingLean.Numbers.Surreal.Normalized.IsNorm
- HeytingLean.Numbers.Surreal.Normalized.NormGame
- HeytingLean.Numbers.Surreal.Normalized.ofGame
- HeytingLean.Numbers.Surreal.Normalized.val
- HeytingLean.Numbers.Surreal.Normalized.zeroN
- HeytingLean.Numbers.Surreal.Normalized.addN
- HeytingLean.Numbers.Surreal.Normalized.mulN
- HeytingLean.Numbers.Surreal.Normalized.add_assoc
- HeytingLean.Numbers.Surreal.Normalized.add_comm
- HeytingLean.Numbers.Surreal.Normalized.zero_add
- HeytingLean.Numbers.Surreal.Normalized.add_zero
- HeytingLean.Numbers.Surreal.Normalized.mul_assoc
Definition
151
Module HeytingLean.Numbers.Surreal.Nucleus.
Lean declarations
- HeytingLean.Numbers.Surreal.Nucleus.canonImage
- HeytingLean.Numbers.Surreal.Nucleus.J
- HeytingLean.Numbers.Surreal.Nucleus.mono_J
- HeytingLean.Numbers.Surreal.Nucleus.idem_J
- HeytingLean.Numbers.Surreal.Nucleus.C
- HeytingLean.Numbers.Surreal.Nucleus.I
- HeytingLean.Numbers.Surreal.Nucleus.mono_I
- HeytingLean.Numbers.Surreal.Nucleus.intReentry
Definition
153
Module HeytingLean.Numbers.Surreal.Operations.
Lean declarations
- HeytingLean.Numbers.Surreal.Operations.one
- HeytingLean.Numbers.Surreal.Operations.negN
- HeytingLean.Numbers.Surreal.Operations.neg
- HeytingLean.Numbers.Surreal.Operations.maxDayList
- HeytingLean.Numbers.Surreal.Operations.day_le_maxDayList_of_mem
- HeytingLean.Numbers.Surreal.Operations.toSigmaList
- HeytingLean.Numbers.Surreal.Operations.L_mkGame_nonempty
- HeytingLean.Numbers.Surreal.Operations.R_mkGame_nonempty
- HeytingLean.Numbers.Surreal.Operations.mkGame
- HeytingLean.Numbers.Surreal.Operations.day_mkGame
- HeytingLean.Numbers.Surreal.Operations.day_mkGame_nonempty
- HeytingLean.Numbers.Surreal.Operations.add
Definition
156
Module HeytingLean.Numbers.Surreal.QuotOps.
Lean declarations
- HeytingLean.Numbers.Surreal.QuotOps.canonicalizeQ_add_comm
- HeytingLean.Numbers.Surreal.QuotOps.canonicalizeQ_add_assoc
- HeytingLean.Numbers.Surreal.QuotOps.canonicalizeQ_add_zero_left
- HeytingLean.Numbers.Surreal.QuotOps.canonicalizeQ_add_zero_right
- HeytingLean.Numbers.Surreal.QuotOps.canonicalizeQ_mul_assoc
- HeytingLean.Numbers.Surreal.QuotOps.canonicalizeQ_mul_left_distrib
- HeytingLean.Numbers.Surreal.QuotOps.canonicalizeQ_mul_right_distrib
- HeytingLean.Numbers.Surreal.QuotOps.canonicalizeQ_mul_zero_left
- HeytingLean.Numbers.Surreal.QuotOps.canonicalizeQ_mul_zero_right
Definition
158
Module HeytingLean.Numbers.SurrealCore.
Lean declarations
- HeytingLean.Numbers.SurrealCore.PreGame
- HeytingLean.Numbers.SurrealCore.maxBirth
- HeytingLean.Numbers.SurrealCore.build
- HeytingLean.Numbers.SurrealCore.truncate
- HeytingLean.Numbers.SurrealCore.canonicalize
- HeytingLean.Numbers.SurrealCore.close
- HeytingLean.Numbers.SurrealCore.canonicalize_idem
- HeytingLean.Numbers.SurrealCore.add
- HeytingLean.Numbers.SurrealCore.neg
- HeytingLean.Numbers.SurrealCore.mul
- HeytingLean.Numbers.SurrealCore.legal_add
- HeytingLean.Numbers.SurrealCore.legal_neg
Definition
159
Module HeytingLean.Ontology.Primordial.
Lean declarations
- HeytingLean.Ontology.Primordial.ReentryKernel
- HeytingLean.Ontology.Primordial.Reentry.kernel
- HeytingLean.Ontology.Primordial.primordialOscillation
- HeytingLean.Ontology.Primordial.oscillation_pair_cancel
- HeytingLean.Ontology.Primordial.dialecticPair
- HeytingLean.Ontology.Primordial.zero_sum
- HeytingLean.Ontology.Primordial.Supported
- HeytingLean.Ontology.Primordial.supported_oscillation
- HeytingLean.Ontology.Primordial.thetaCycle_zero_sum
- HeytingLean.Ontology.Primordial.thetaCycle_supported_cancel
Definition
164
Module HeytingLean.Payments.CLI.PMTests.
Lean declarations
- HeytingLean.Payments.CLI.PMTests.policyFormula4
- HeytingLean.Payments.CLI.PMTests.env4
- HeytingLean.Payments.CLI.PMTests.mkPolicy
- HeytingLean.Payments.CLI.PMTests.mkState
- HeytingLean.Payments.CLI.PMTests.mkReq
- HeytingLean.Payments.CLI.PMTests.assert
- HeytingLean.Payments.CLI.PMTests.testHappy
- HeytingLean.Payments.CLI.PMTests.testPerTxFail
- HeytingLean.Payments.CLI.PMTests.testPerDayFail
- HeytingLean.Payments.CLI.PMTests.testBudgetFail
- HeytingLean.Payments.CLI.PMTests.main
- HeytingLean.Payments.CLI.PMTests.main
Definition
165
Module HeytingLean.Payments.CLI.PMVerify.
Lean declarations
- HeytingLean.Payments.CLI.PMVerify.policyFormula4
- HeytingLean.Payments.CLI.PMVerify.env4
- HeytingLean.Payments.CLI.PMVerify.Public
- HeytingLean.Payments.CLI.PMVerify.parsePublicE
- HeytingLean.Payments.CLI.PMVerify.Certificate
- HeytingLean.Payments.CLI.PMVerify.parseCertificateE
- HeytingLean.Payments.CLI.PMVerify.main
- HeytingLean.Payments.CLI.PMVerify.main
Definition
167
Module HeytingLean.Payments.ContractModel.
Lean declarations
- HeytingLean.Payments.ContractModel.Pub
- HeytingLean.Payments.ContractModel.Pins
- HeytingLean.Payments.ContractModel.PMCall
- HeytingLean.Payments.ContractModel.PMState
- HeytingLean.Payments.ContractModel.Reject
- HeytingLean.Payments.ContractModel.Membership
- HeytingLean.Payments.ContractModel.member
- HeytingLean.Payments.ContractModel.stmtHashOf
- HeytingLean.Payments.ContractModel.step
Definition
170
Module HeytingLean.Payments.Types.
Lean declarations
- HeytingLean.Payments.Types.Budget
- HeytingLean.Payments.Types.Policy
- HeytingLean.Payments.Types.BudgetSpend
- HeytingLean.Payments.Types.State
- HeytingLean.Payments.Types.Request
- HeytingLean.Payments.Types.getStr
- HeytingLean.Payments.Types.getNat
- HeytingLean.Payments.Types.getArr
- HeytingLean.Payments.Types.optStr
- HeytingLean.Payments.Types.optNat
- HeytingLean.Payments.Types.parseBudget
- HeytingLean.Payments.Types.parsePolicy
Definition
172
Module HeytingLean.ProofWidgets.LoFViz.Kernel.
Lean declarations
- HeytingLean.ProofWidgets.LoFViz.Kernel.contains
- HeytingLean.ProofWidgets.LoFViz.Kernel.insert
- HeytingLean.ProofWidgets.LoFViz.Kernel.erase
- HeytingLean.ProofWidgets.LoFViz.Kernel.union
- HeytingLean.ProofWidgets.LoFViz.Kernel.inter
- HeytingLean.ProofWidgets.LoFViz.Kernel.diff
- HeytingLean.ProofWidgets.LoFViz.Kernel.subset
- HeytingLean.ProofWidgets.LoFViz.Kernel.equal
- HeytingLean.ProofWidgets.LoFViz.Kernel.CertificateBundle
- HeytingLean.ProofWidgets.LoFViz.Kernel.Aggregate
- HeytingLean.ProofWidgets.LoFViz.Kernel.closure
- HeytingLean.ProofWidgets.LoFViz.Kernel.step
Definition
173
Module HeytingLean.ProofWidgets.LoFViz.Proof.Core.
Lean declarations
- HeytingLean.ProofWidgets.LoFViz.Proof.Core.defaultFuel
- HeytingLean.ProofWidgets.LoFViz.Proof.Core.nameFromString
- HeytingLean.ProofWidgets.LoFViz.Proof.Core.TermBuildM
- HeytingLean.ProofWidgets.LoFViz.Proof.Core.primitiveKind
- HeytingLean.ProofWidgets.LoFViz.Proof.Core.primitiveLabel
- HeytingLean.ProofWidgets.LoFViz.Proof.Core.journalGraph
- HeytingLean.ProofWidgets.LoFViz.Proof.Core.buildProofGraph
- HeytingLean.ProofWidgets.LoFViz.Proof.Core.Handle
- HeytingLean.ProofWidgets.LoFViz.Proof.Core.Normalized
- HeytingLean.ProofWidgets.LoFViz.Proof.Core.VisualizationBundle
- HeytingLean.ProofWidgets.LoFViz.Proof.Core.constantProofExpr
- HeytingLean.ProofWidgets.LoFViz.Proof.Core.Normalized.ofConstantCore
Definition
174
Module HeytingLean.ProofWidgets.LoFViz.Proof.Graph.
Lean declarations
- HeytingLean.ProofWidgets.LoFViz.Proof.Graph.NodeId
- HeytingLean.ProofWidgets.LoFViz.Proof.Graph.NodeKind
- HeytingLean.ProofWidgets.LoFViz.Proof.Graph.toString
- HeytingLean.ProofWidgets.LoFViz.Proof.Graph.PrimitiveKind
- HeytingLean.ProofWidgets.LoFViz.Proof.Graph.toString
- HeytingLean.ProofWidgets.LoFViz.Proof.Graph.Node
- HeytingLean.ProofWidgets.LoFViz.Proof.Graph.EdgeKind
- HeytingLean.ProofWidgets.LoFViz.Proof.Graph.toString
- HeytingLean.ProofWidgets.LoFViz.Proof.Graph.Edge
- HeytingLean.ProofWidgets.LoFViz.Proof.Graph.ProofGraph
- HeytingLean.ProofWidgets.LoFViz.Proof.Graph.pushNode
- HeytingLean.ProofWidgets.LoFViz.Proof.Graph.pushEdge
Definition
178
Module HeytingLean.ProofWidgets.LoFViz.Render.Models.
Lean declarations
- HeytingLean.ProofWidgets.LoFViz.Render.Models.BoundaryModel
- HeytingLean.ProofWidgets.LoFViz.Render.Models.BoundaryModel.fromKernel
- HeytingLean.ProofWidgets.LoFViz.Render.Models.HyperNode
- HeytingLean.ProofWidgets.LoFViz.Render.Models.HyperEdge
- HeytingLean.ProofWidgets.LoFViz.Render.Models.HypergraphModel
- HeytingLean.ProofWidgets.LoFViz.Render.Models.HypergraphModel.fromKernel
Definition
183
Module HeytingLean.ProofWidgets.LoFViz.State.
Lean declarations
- HeytingLean.ProofWidgets.LoFViz.State.Primitive
- HeytingLean.ProofWidgets.LoFViz.State.DialStage
- HeytingLean.ProofWidgets.LoFViz.State.VisualMode
- HeytingLean.ProofWidgets.LoFViz.State.Lens
- HeytingLean.ProofWidgets.LoFViz.State.EventKind
- HeytingLean.ProofWidgets.LoFViz.State.Event
- HeytingLean.ProofWidgets.LoFViz.State.JournalEntry
- HeytingLean.ProofWidgets.LoFViz.State.State
- HeytingLean.ProofWidgets.LoFViz.State.initialState
- HeytingLean.ProofWidgets.LoFViz.State.applyPrimitive
- HeytingLean.ProofWidgets.LoFViz.State.applyEvent
Definition
184
Module HeytingLean.ProofWidgets.LoFViz.Tests.
Lean declarations
- HeytingLean.ProofWidgets.LoFViz.Tests.kernelSummary_ne_empty
- HeytingLean.ProofWidgets.LoFViz.Tests.certificates_have_default_message
- HeytingLean.ProofWidgets.LoFViz.Tests.notes_nonempty
- HeytingLean.ProofWidgets.LoFViz.Tests.fiberNotes_length
- HeytingLean.ProofWidgets.LoFViz.Tests.fiberNotes_contains_transport
- HeytingLean.ProofWidgets.LoFViz.Tests.boundary_and_hypergraph_share_activity
- HeytingLean.ProofWidgets.LoFViz.Tests.boundary_radius_formula
- HeytingLean.ProofWidgets.LoFViz.Tests.hypergraph_reentry_matches_kernel
Definition
194
Module HeytingLean.Tests.Compliance.
Lean declarations
- HeytingLean.Tests.Compliance.identity_round_verified
- HeytingLean.Tests.Compliance.tensor_shadow_verified
- HeytingLean.Tests.Compliance.tensor_rt2_verified
- HeytingLean.Tests.Compliance.tensor_round_verified
- HeytingLean.Tests.Compliance.tensor_intensity_round_verified
- HeytingLean.Tests.Compliance.runtime_tensor_round_verified
- HeytingLean.Tests.Compliance.graph_shadow_verified
- HeytingLean.Tests.Compliance.graph_rt2_verified
- HeytingLean.Tests.Compliance.graph_alexandroff_round_verified
- HeytingLean.Tests.Compliance.runtime_graph_round_verified
- HeytingLean.Tests.Compliance.graph_alexandroff_process_collapse
- HeytingLean.Tests.Compliance.graph_alexandroff_process_expand
Definition
229
Module HeytingLean.Topos.LTfromNucleus.
Lean declarations
- HeytingLean.Topos.LTfromNucleus.LawvereTierney
- HeytingLean.Topos.LTfromNucleus.ofClosureFamily
- HeytingLean.Topos.LTfromNucleus.reclassify_id
- HeytingLean.Topos.LTfromNucleus.chi_pullback_char
- HeytingLean.Topos.LTfromNucleus.reclassifyWith_pullback_naturality
- HeytingLean.Topos.LTfromNucleus.reclassify_pullback_naturality
- HeytingLean.Topos.LTfromNucleus.LawvereTierneyKit
- HeytingLean.Topos.LTfromNucleus.reclassify_le_of_le
- HeytingLean.Topos.LTfromNucleus.reclassify_monotone
- HeytingLean.Topos.LTfromNucleus.reclassify_idem
- HeytingLean.Topos.LTfromNucleus.ofLawvereTierney
- HeytingLean.Topos.LTfromNucleus.ofClassifier