inductive
definition
SkewUnit
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Measurement.RSNative.Core on GitHub at line 195.
browse module
All declarations in this module, on Recognition.
explainer page
used by
formal source
192inductive CohUnit : Type
193inductive ActUnit : Type
194inductive CostUnit : Type
195inductive SkewUnit : Type
196inductive MeaningUnit : Type
197inductive QualiaUnit : Type
198inductive ZUnit : Type
199
200abbrev Tick := Quantity TickUnit
201abbrev Voxel := Quantity VoxelUnit
202abbrev Coh := Quantity CohUnit
203abbrev Act := Quantity ActUnit
204abbrev Cost := Quantity CostUnit
205abbrev Skew := Quantity SkewUnit
206abbrev Meaning := Quantity MeaningUnit
207abbrev Qualia := Quantity QualiaUnit
208abbrev ZCharge := Quantity ZUnit
209
210end RSNative
211end Measurement
212end IndisputableMonolith