This PR bumps Grove to the latest revision and starts adding data about the `String` library. Just a small start, more to come.
24 lines
924 B
Text
24 lines
924 B
Text
import Grove.Framework
|
|
import GroveStdlib.Generated.«associative-query-operations»
|
|
import GroveStdlib.Generated.«associative-creation-operations»
|
|
import GroveStdlib.Generated.«associative-modification-operations»
|
|
import GroveStdlib.Generated.«associative-create-then-query»
|
|
import GroveStdlib.Generated.«associative-all-operations-covered»
|
|
import GroveStdlib.Generated.«slice-producing»
|
|
|
|
/-
|
|
This file is autogenerated by grove. You can manually edit it, for example to resolve merge
|
|
conflicts, but be careful.
|
|
-/
|
|
|
|
open Grove.Framework Widget
|
|
|
|
namespace GroveStdlib.Generated
|
|
|
|
def restoreState : RestoreStateM Unit := do
|
|
«associative-query-operations».restoreState
|
|
«associative-creation-operations».restoreState
|
|
«associative-modification-operations».restoreState
|
|
«associative-create-then-query».restoreState
|
|
«associative-all-operations-covered».restoreState
|
|
«slice-producing».restoreState
|