`IndisputableMonolith.Relativity.ILG.Params`

IndisputableMonolith/Relativity/ILG/Params.lean · 19 lines · 2 declarations

Explainer status: pending

   1import Mathlib
   2
   3namespace IndisputableMonolith
   4namespace Relativity
   5namespace ILG
   6
   7/-- Minimal parameter record used by downstream modules. -/
   8structure Params where
   9  alpha : ℝ := 1
  10  Clag  : ℝ := 0
  11
  12structure ParamProps (P : Params) : Prop :=
  13  (alpha_nonneg : 0 ≤ P.alpha)
  14  (Clag_nonneg : 0 ≤ P.Clag)
  15
  16end ILG
  17end Relativity
  18end IndisputableMonolith
  19

source mirrored from github.com/jonwashburn/shape-of-logic