- sizeOf : α → Nat
Instances
- instSizeOf
- IO.Error._sizeOf_inst
- Nat.SOM.Expr._sizeOf_inst
- IO.FS.Metadata._sizeOf_inst
- ByteArray._sizeOf_inst
- ST.Ref._sizeOf_inst
- UInt32._sizeOf_inst
- Lean.Meta.Simp.Config._sizeOf_inst
- UInt8._sizeOf_inst
- ForInStep._sizeOf_inst
- Substring._sizeOf_inst
- StdGen._sizeOf_inst
- IO.FS.Stream._sizeOf_inst
- Socket.ShutdownHow._sizeOf_inst
- IO.FS.FileType._sizeOf_inst
- Lean.Meta.Rewrite.Config._sizeOf_inst
- Sigma._sizeOf_inst
- DoResultPR._sizeOf_inst
- FloatSpec._sizeOf_inst
- Std.Format._sizeOf_inst
- IO.Process.Stdio._sizeOf_inst
- EStateM.Result._sizeOf_inst
- Lean.Data.AC.Context._sizeOf_inst
- DoResultBC._sizeOf_inst
- Subtype._sizeOf_inst
- IO.FS.SystemTime._sizeOf_inst
- PUnit._sizeOf_inst
- Option._sizeOf_inst
- _private.Init.Data.Format.Basic.0.Std.Format.State._sizeOf_inst
- Std.Range._sizeOf_inst
- Lean.Syntax._sizeOf_inst
- _private.Init.Data.Format.Basic.0.Std.Format.WorkGroup._sizeOf_inst
- UInt64._sizeOf_inst
- IO.FS.DirEntry._sizeOf_inst
- Nat.Linear.Expr._sizeOf_inst
- DoResultSBC._sizeOf_inst
- Lean.Meta.EtaStructMode._sizeOf_inst
- UInt16._sizeOf_inst
- IO.Process.Child._sizeOf_inst
- Nat.Linear.ExprCnstr._sizeOf_inst
- Std.Format.FlattenBehavior._sizeOf_inst
- Lean.Meta.DSimp.Config._sizeOf_inst
- Lean.NameGenerator._sizeOf_inst
- Lean.Data.AC.Expr._sizeOf_inst
- PSum._sizeOf_inst
- String.Iterator._sizeOf_inst
- String.instSizeOfIterator
- List._sizeOf_inst
- Subarray._sizeOf_inst
- IO.FS.Stream.Buffer._sizeOf_inst
- DoResultPRBC._sizeOf_inst
- Sum._sizeOf_inst
- Thunk._sizeOf_inst
- Nat.Linear.PolyCnstr._sizeOf_inst
- Float._sizeOf_inst
- instSizeOfNat
- Lean.Data.AC.Variable._sizeOf_inst
- _private.Init.Data.Format.Basic.0.Std.Format.SpaceResult._sizeOf_inst
- Lean.Meta.TransparencyMode._sizeOf_inst
- IO.AccessRight._sizeOf_inst
- _private.Init.Data.Format.Basic.0.Std.Format.WorkItem._sizeOf_inst
- IO.Process.SpawnArgs._sizeOf_inst
- Socket.SockType._sizeOf_inst
- PNonScalar._sizeOf_inst
- Socket.AddressFamily._sizeOf_inst
- Array._sizeOf_inst
- IO.Process.Output._sizeOf_inst
- IO.FS.Mode._sizeOf_inst
- IO.FileRight._sizeOf_inst
- Prod._sizeOf_inst
- Lean.Loop._sizeOf_inst
- System.FilePath._sizeOf_inst
- PSigma._sizeOf_inst
- Lean.Module._sizeOf_inst
- Bool._sizeOf_inst
- Lean.Meta.Simp.ConfigCtx._sizeOf_inst
- FloatArray._sizeOf_inst
- Except._sizeOf_inst
- Ordering._sizeOf_inst
- Lean.instSizeOfName
- String._sizeOf_inst
- Task._sizeOf_inst
- USize._sizeOf_inst
- NonScalar._sizeOf_inst
- IO.Process.StdioConfig._sizeOf_inst
- Char._sizeOf_inst
- Fin._sizeOf_inst
- Int._sizeOf_inst
- instSizeOfForAllUnit
Equations
- default.sizeOf α _fun_discr = match _fun_discr with | x => 0
Equations
- instSizeOf α = { sizeOf := default.sizeOf α }
Equations
- Lean.Name.sizeOf Lean.Name.anonymous = 1
- Lean.Name.sizeOf (Lean.Name.str p s a) = 1 + Lean.Name.sizeOf p + sizeOf s
- Lean.Name.sizeOf (Lean.Name.num p n a) = 1 + Lean.Name.sizeOf p + sizeOf n
Equations
- Lean.instSizeOfName = { sizeOf := fun n => Lean.Name.sizeOf n }