Documentation

Init.Data.String.Csimp

This module contains csimp lemmas used to optimize String functions.

source
def String.toListImpl (s : String) :
List Char
Equations
Instances For
    source
    @[csimp]
    theorem String.toList_eq_toListImpl :
    toList = toListImpl