Documentation

Init.Data.Nat.SOM

@[inline]
abbrev Nat.SOM.Mon :
Type
Equations
def Nat.SOM.Mon.mul.go (fuel : Nat) (m₁ : Nat.SOM.Mon) (m₂ : Nat.SOM.Mon) :
Equations
@[inline]
abbrev Nat.SOM.Poly :
Type
Equations
Equations
Equations
Equations
Equations
Equations