val char_t_of_char (c: char) : Type0
val char_t_of_char (c: char) : Type0
let char_t_of_char (c: char): Type0 =
  match c with
  | 'a' -> ca
  | 'b' -> cb
  | 'c' -> cc
  | 'd' -> cd
  | 'e' -> ce
  | 'f' -> cf
  | 'g' -> cg
  | 'h' -> ch
  | 'i' -> ci
  | 'j' -> cj
  | 'k' -> ck
  | 'l' -> cl
  | 'm' -> cm
  | 'n' -> cn
  | 'o' -> co
  | 'p' -> cp
  | 'q' -> cq
  | 'r' -> cr
  | 's' -> cs
  | 't' -> ct
  | 'u' -> cu
  | 'v' -> cv
  | 'w' -> cw
  | 'x' -> cx
  | 'y' -> cy
  | 'z' -> cz
  | 'A' -> cA
  | 'B' -> cB
  | 'C' -> cC
  | 'D' -> cD
  | 'E' -> cE
  | 'F' -> cF
  | 'G' -> cG
  | 'H' -> cH
  | 'I' -> cI
  | 'J' -> cJ
  | 'K' -> cK
  | 'L' -> cL
  | 'M' -> cM
  | 'N' -> cN
  | 'O' -> cO
  | 'P' -> cP
  | 'Q' -> cQ
  | 'R' -> cR
  | 'S' -> cS
  | 'T' -> cT
  | 'U' -> cU
  | 'V' -> cV
  | 'W' -> cW
  | 'X' -> cX
  | 'Y' -> cY
  | 'Z' -> cZ
  | '0' -> c0
  | '1' -> c1
  | '2' -> c2
  | '3' -> c3
  | '4' -> c4
  | '5' -> c5
  | '6' -> c6
  | '7' -> c7
  | '8' -> c8
  | '9' -> c9
  | '_' -> c_
  | '.' -> cdot
  | _ -> c_
module Steel.C.Typestring

(** Suppose [struct (t : string) (fields : struct_fields)] represents the type of struct values.
    Then, when extracting values of type [ref (struct t fields)], the tag t is lost.
    To make sure this information sticks around, this module provides
    an encoding of strings like t as types. *)

val ca: Type0
val cb: Type0
val cc: Type0
val cd: Type0
val ce: Type0
val cf: Type0
val cg: Type0
val ch: Type0
val ci: Type0
val cj: Type0
val ck: Type0
val cl: Type0
val cm: Type0
val cn: Type0
val co: Type0
val cp: Type0
val cq: Type0
val cr: Type0
val cs: Type0
val ct: Type0
val cu: Type0
val cv: Type0
val cw: Type0
val cx: Type0
val cy: Type0
val cz: Type0
val cA: Type0
val cB: Type0
val cC: Type0
val cD: Type0
val cE: Type0
val cF: Type0
val cG: Type0
val cH: Type0
val cI: Type0
val cJ: Type0
val cK: Type0
val cL: Type0
val cM: Type0
val cN: Type0
val cO: Type0
val cP: Type0
val cQ: Type0
val cR: Type0
val cS: Type0
val cT: Type0
val cU: Type0
val cV: Type0
val cW: Type0
val cX: Type0
val cY: Type0
val cZ: Type0
val c0: Type0
val c1: Type0
val c2: Type0
val c3: Type0
val c4: Type0
val c5: Type0
val c6: Type0
val c7: Type0
val c8: Type0
val c9: Type0
val c_: Type0
val cdot: Type0

val string_nil: Type0
val string_cons (c: Type0) (s: Type0): Type0

open FStar.String
/
prims.fst.checked FStar.Tactics.fst.checked FStar.String.fsti.checked FStar.Pervasives.fsti.checked
Steel.C.Typestring.fsti
c: FStar.String.char -> Type0
FStar.String.char Steel.C.Typestring.ca Steel.C.Typestring.cb Steel.C.Typestring.cc Steel.C.Typestring.cd Steel.C.Typestring.ce Steel.C.Typestring.cf Steel.C.Typestring.cg Steel.C.Typestring.ch Steel.C.Typestring.ci Steel.C.Typestring.cj Steel.C.Typestring.ck Steel.C.Typestring.cl Steel.C.Typestring.cm Steel.C.Typestring.cn Steel.C.Typestring.co Steel.C.Typestring.cp Steel.C.Typestring.cq Steel.C.Typestring.cr Steel.C.Typestring.cs Steel.C.Typestring.ct Steel.C.Typestring.cu Steel.C.Typestring.cv Steel.C.Typestring.cw Steel.C.Typestring.cx Steel.C.Typestring.cy Steel.C.Typestring.cz Steel.C.Typestring.cA Steel.C.Typestring.cB Steel.C.Typestring.cC Steel.C.Typestring.cD Steel.C.Typestring.cE Steel.C.Typestring.cF Steel.C.Typestring.cG Steel.C.Typestring.cH Steel.C.Typestring.cI Steel.C.Typestring.cJ Steel.C.Typestring.cK Steel.C.Typestring.cL Steel.C.Typestring.cM Steel.C.Typestring.cN Steel.C.Typestring.cO Steel.C.Typestring.cP Steel.C.Typestring.cQ Steel.C.Typestring.cR Steel.C.Typestring.cS Steel.C.Typestring.cT Steel.C.Typestring.cU Steel.C.Typestring.cV Steel.C.Typestring.cW Steel.C.Typestring.cX Steel.C.Typestring.cY Steel.C.Typestring.cZ Steel.C.Typestring.c0 Steel.C.Typestring.c1 Steel.C.Typestring.c2 Steel.C.Typestring.c3 Steel.C.Typestring.c4 Steel.C.Typestring.c5 Steel.C.Typestring.c6 Steel.C.Typestring.c7 Steel.C.Typestring.c8 Steel.C.Typestring.c9 Steel.C.Typestring.c_ Steel.C.Typestring.cdot FStar.Char.char
let char_t_of_char (c: char) : Type0 =
  
match c with
| 'a' -> ca
| 'b' -> cb
| 'c' -> cc
| 'd' -> cd
| 'e' -> ce
| 'f' -> cf
| 'g' -> cg
| 'h' -> ch
| 'i' -> ci
| 'j' -> cj
| 'k' -> ck
| 'l' -> cl
| 'm' -> cm
| 'n' -> cn
| 'o' -> co
| 'p' -> cp
| 'q' -> cq
| 'r' -> cr
| 's' -> cs
| 't' -> ct
| 'u' -> cu
| 'v' -> cv
| 'w' -> cw
| 'x' -> cx
| 'y' -> cy
| 'z' -> cz
| 'A' -> cA
| 'B' -> cB
| 'C' -> cC
| 'D' -> cD
| 'E' -> cE
| 'F' -> cF
| 'G' -> cG
| 'H' -> cH
| 'I' -> cI
| 'J' -> cJ
| 'K' -> cK
| 'L' -> cL
| 'M' -> cM
| 'N' -> cN
| 'O' -> cO
| 'P' -> cP
| 'Q' -> cQ
| 'R' -> cR
| 'S' -> cS
| 'T' -> cT
| 'U' -> cU
| 'V' -> cV
| 'W' -> cW
| 'X' -> cX
| 'Y' -> cY
| 'Z' -> cZ
| '0' -> c0
| '1' -> c1
| '2' -> c2
| '3' -> c3
| '4' -> c4
| '5' -> c5
| '6' -> c6
| '7' -> c7
| '8' -> c8
| '9' -> c9
| '_' -> c_
| '.' -> cdot
| _ -> c_