`LeanCode`

definition

show as: view math explainer →

module: IndisputableMonolith.RRF.Foundation.SelfReference
domain: RRF
line: 30 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.RRF.Foundation.SelfReference on GitHub at line 30.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  27/-! ## Code as Recognition -/
  28
  29/-- Lean code that can be type-checked. -/
  30structure LeanCode where
  31  /-- The source code (as a string). -/
  32  source : String
  33  /-- The module name. -/
  34  module : String
  35
  36/-- The result of type-checking code. -/
  37inductive TypeCheckResult
  38  | success : TypeCheckResult
  39  | failure (error : String) : TypeCheckResult
  40
  41/-- A self-referential code structure. -/
  42structure SelfReferentialCode where
  43  /-- The code being analyzed. -/
  44  code : LeanCode
  45  /-- The code compiles (type-checks). -/
  46  compiles : TypeCheckResult
  47  /-- The code refers to itself (as a proposition).
  48      Refined: check if source contains module name. -/
  49  self_referential : code.source.contains code.module.toSubstring
  50
  51/-- If code compiles, it is "recognized" (valid in the type theory). -/
  52def isRecognized (s : SelfReferentialCode) : Bool :=
  53  match s.compiles with
  54  | .success => true
  55  | .failure _ => false
  56
  57/-! ## The Meta-RRF Structure -/
  58
  59/-- A description of the RRF in Lean. -/
  60structure RRFDescription where

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.