Representing units / dimensional analysis?

Stream: general

[Lhr]

In other languages you can use branded opaque types for representing units like seconds or minutes. In F# you can parameterize the builtin scalar types by a unit, Int<Second> or something like that.

What would be the recommended way for encoding units and doing dimensional analysis in lean4? Thanks

[Niels Voss]

You might be interested in https://leanprover.zulipchat.com/#narrow/channel/479953-PhysLean/topic/physical.20units/with/547978619