The ToSlice typeclass

class String.ToSlice (α : Type u) : Type u

Typeclass for types that have a conversion function to String.Slice. This typeclass is used to make some String/String.Slice functions polymorphic. As such, for now it is not intended that there instances of this beyond ToSlice String and ToSlice String.Slice.

To convert arbitrary data into a string representation, see ToString and Repr.

• toSlice : α → Slice

@[inline]

instance String.instToSliceSlice : ToSlice Slice

Equations

• String.instToSliceSlice = { toSlice := id }

@[inline]

instance String.instToSlice : ToSlice String

Equations

• String.instToSlice = { toSlice := String.toSlice }