val byte_of_hex: a:hex_digit -> b:hex_digit -> int
let byte_of_hex a b =
  FStar.Mul.(int_of_hex a * 16 + int_of_hex b)
val byte_of_hex: a:hex_digit -> b:hex_digit -> int
let byte_of_hex a b =
let open FStar.Mul in int_of_hex a * 16 + int_of_hex b
Lib.Meta.fst.checked
prims.fst.checked Lib.IntTypes.fsti.checked FStar.String.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked FStar.List.fst.checked FStar.Char.fsti.checked
Lib.Meta.fst
Lib.Meta.hex_digit Prims.op_Addition FStar.Mul.op_Star Lib.Meta.int_of_hex Prims.int
module Lib.Meta

open Lib.IntTypes

/// Helpers used in tests and tactics (see e.g. Test.LowStarize)

#set-options "--max_fuel 0 --max_ifuel 0 --z3rlimit 50"


val is_hex_digit: Char.char -> bool
let is_hex_digit = function
  | '0'
  | '1'
  | '2'
  | '3'
  | '4'
  | '5'
  | '6'
  | '7'
  | '8'
  | '9'
  | 'a' | 'A'
  | 'b' | 'B'
  | 'c' | 'C'
  | 'd' | 'D'
  | 'e' | 'E'
  | 'f' | 'F' -> true
  | _ -> false


type hex_digit = c:Char.char{is_hex_digit c}


val int_of_hex: c:hex_digit -> int
let int_of_hex = function
  | '0' -> 0
  | '1' -> 1
  | '2' -> 2
  | '3' -> 3
  | '4' -> 4
  | '5' -> 5
  | '6' -> 6
  | '7' -> 7
  | '8' -> 8
  | '9' -> 9
  | 'a' | 'A' -> 10
  | 'b' | 'B' -> 11
  | 'c' | 'C' -> 12
  | 'd' | 'D' -> 13
  | 'e' | 'E' -> 14
  | 'f' | 'F' -> 15


val byte_of_hex: a:hex_digit -> b:hex_digit -> int
val byte_of_hex: a:hex_digit -> b:hex_digit -> int
a: Lib.Meta.hex_digit -> b: Lib.Meta.hex_digit -> Prims.int