module
module
IndisputableMonolith.Measurement.RSNative.Core
show as:
view Lean formalization →
used by (3)
depends on (1)
declarations in this module (41)
-
inductive
Status -
structure
Protocol -
def
hygienic -
def
hygienicBool -
structure
Window -
def
instant -
def
stop -
inductive
Uncertainty -
def
sigmaVal -
def
intervalBounds -
structure
Measurement -
def
map -
def
mapWithProtocol -
def
mapUncertainty -
def
addNote -
def
addNotes -
abbrev
Observable -
structure
Quantity -
theorem
val_zero -
theorem
val_add -
theorem
val_sub -
theorem
val_neg -
theorem
val_smul -
inductive
TickUnit -
inductive
VoxelUnit -
inductive
CohUnit -
inductive
ActUnit -
inductive
CostUnit -
inductive
SkewUnit -
inductive
MeaningUnit -
inductive
QualiaUnit -
inductive
ZUnit -
abbrev
Tick -
abbrev
Voxel -
abbrev
Coh -
abbrev
Act -
abbrev
Cost -
abbrev
Skew -
abbrev
Meaning -
abbrev
Qualia -
abbrev
ZCharge