`IndisputableMonolith.ILG.ParamsKernel`

IndisputableMonolith/ILG/ParamsKernel.lean · 16 lines · 2 declarations

Explainer status: pending

   1import Mathlib
   2import IndisputableMonolith.ILG.Params
   3
   4namespace IndisputableMonolith
   5namespace ILG
   6
   7/-- Verification predicate for the parameter kernel: parameters must be well-formed. -/
   8def ParamsKernelVerified (P : Params) : Prop :=
   9  ParamProps P
  10
  11@[simp] lemma paramsKernel_verified_any (P : Params) (h : ParamProps P) : ParamsKernelVerified P := h
  12
  13
  14end ILG
  15end IndisputableMonolith
  16

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