module module

`IndisputableMonolith.Foundation.SeamClosure.Reference`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Basic module_import

declarations in this module (18)

structure ReferringTrace L44
def refersTo L54
instance instDecidableRefersTo L66
def selfReference L72
theorem selfReference_not_refers L76
def stepReference L85
inductive Generated L93
theorem generated_all L105
theorem reference_reduces_to_distinction L127
structure receiving L138
structure ReferringAlgebra L141
def evalGround L148
def eval L154
theorem eval_ground_step L160
def IsHom L172
def evalHom L178
theorem evalHom_isHom L181
theorem reference_forced_by_distinction L197