IndisputableMonolith.CPM.LNALBridge

   1import Mathlib
   2import IndisputableMonolith.LNAL.Compiler
   3
   4namespace IndisputableMonolith
   5namespace CPM
   6
   7open IndisputableMonolith.LNAL
   8
   9/-- A minimal structured-set surrogate: programs that pass static checks. -/
  10def Structured (src : String) : Bool :=
  11  let rep := staticChecks (match parseProgram src with
  12    | .ok code   => code
  13    | .error _   => #[])
  14  rep.ok
  15
  16/-- A toy defect functional (zero when checks pass). -/
  17def Defect (src : String) : Nat := if Structured src then 0 else 1
  18
  19end CPM
  20end IndisputableMonolith
  21