Commit 2021-05-09 05:35 b45b7b60

View on Github →

feat(*): dumping my ForMathlib collection

Estimated changes

Created Mathlib/Data/ByteArray.lean

added def ByteArray.toSlice

added def ByteArray.toSliceT

added def ByteSlice.forIn.loop

added def ByteSlice.getOp

added def ByteSlice.toArray

added def ByteSlice.toString

added structure ByteSlice

added def ByteSliceT.getOp

added def ByteSliceT.size

added def ByteSliceT.toSlice

added structure ByteSliceT

added def String.toAsciiByteArray.loop

added def String.toAsciiByteArray

Created Mathlib/Data/Char.lean

added def Char.toUInt8

added theorem Char.utf8Size_pos

added theorem String.csize_pos

Created Mathlib/Data/List/Basic.lean

added def List.mem

added theorem List.mem_append

added theorem List.mem_bind

added theorem List.mem_join

added theorem List.mem_map

Created Mathlib/Data/Nat/Basic.lean

added theorem Nat.Up.WF

added theorem Nat.Up.next

added def Nat.Up

Created Mathlib/Data/UInt.lean

added theorem Fin.val_eq_of_lt

added theorem UInt32.val_eq_of_lt

added def UInt8.isAlpha

added def UInt8.isAlphanum

added def UInt8.isDigit

added def UInt8.isLower

added def UInt8.isUpper

added def UInt8.toChar

added theorem UInt8.toChar_aux

Modified Mathlib/Logic/Basic.lean

added theorem Or.imp_right

added theorem Or.symm

added theorem or_assoc