// SPDX-FileCopyrightText: Chris Pressey, the original author of this work, has dedicated it to the public domain.
// For more information, please refer to <https://unlicense.org/>
// SPDX-License-Identifier: Unlicense

module StringJazz

open FStar.String

let s = "These"

let _ = assert (s = "These")

let _ = assert ((lowercase "These") = "these")

// You might think this should work, but it seems
// `assert` is not powerful enough for this job:
//
// let _ = assert ((lowercase s) = "these")

// One can ask F* to reduce the expression
// `lowercase s` to its simplest form instead.
// This is powerful enough to do the job:

let proof_of_lowercase ()
  : Lemma ((lowercase s) = "these")
  = normalize_term_spec (lowercase s)