val compare_const (c1 c2: vconst) : order
val compare_const (c1 c2: vconst) : order
let compare_const (c1 c2 : vconst) : order =
    match c1, c2 with
    | C_Unit, C_Unit -> Eq
    | C_Int i, C_Int j -> order_from_int (i - j)
    | C_True, C_True -> Eq
    | C_False, C_False -> Eq
    | C_String s1, C_String s2 -> order_from_int (compare_string s1 s2)
    | C_Range r1, C_Range r2 -> Eq
    | C_Reify, C_Reify -> Eq
    | C_Reflect l1, C_Reflect l2 -> compare_name l1 l2
    | C_Unit,  _ -> Lt       | _, C_Unit  -> Gt
    | C_Int _, _ -> Lt       | _, C_Int _ -> Gt
    | C_True,  _ -> Lt       | _, C_True  -> Gt
    | C_False, _ -> Lt       | _, C_False -> Gt
    | C_String _, _ -> Lt    | _, C_String _ -> Gt
    | C_Range _, _ -> Lt     | _, C_Range _ -> Gt
    | C_Reify, _ -> Lt       | _, C_Reify -> Gt
    | C_Reflect _, _ -> Lt   | _, C_Reflect _ -> Gt
(*
   Copyright 2008-2018 Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)
module FStar.Reflection.V1.Compare

open FStar.Stubs.Reflection.Types
open FStar.Stubs.Reflection.V1.Data
open FStar.Stubs.Reflection.V1.Builtins
open FStar.Reflection.V1.Derived
open FStar.Order

let compare_name (n1 n2 : name) : order =
    compare_list n1 n2 (fun s1 s2 -> order_from_int (compare_string s1 s2))

let compare_fv (f1 f2 : fv) : order =
    compare_name (inspect_fv f1) (inspect_fv f2)
/
prims.fst.checked FStar.Stubs.Reflection.V1.Data.fsti.checked FStar.Stubs.Reflection.V1.Builtins.fsti.checked FStar.Stubs.Reflection.Types.fsti.checked FStar.Reflection.V1.Derived.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Order.fst.checked
FStar.Reflection.V1.Compare.fst
c1: FStar.Stubs.Reflection.V1.Data.vconst -> c2: FStar.Stubs.Reflection.V1.Data.vconst
  -> FStar.Order.order
FStar.Stubs.Reflection.V1.Data.vconst FStar.Pervasives.Native.Mktuple2 FStar.Order.Eq Prims.int FStar.Order.order_from_int Prims.op_Subtraction Prims.string FStar.Stubs.Reflection.V1.Builtins.compare_string FStar.Range.range FStar.Stubs.Reflection.Types.name FStar.Reflection.V1.Compare.compare_name FStar.Order.Lt FStar.Order.Gt FStar.Order.order
let compare_const (c1 c2: vconst) : order =
  
match c1, c2 with
| C_Unit, C_Unit -> Eq
| C_Int i, C_Int j -> order_from_int (i - j)
| C_True, C_True -> Eq
| C_False, C_False -> Eq
| C_String s1, C_String s2 -> order_from_int (compare_string s1 s2)
| C_Range r1, C_Range r2 -> Eq
| C_Reify, C_Reify -> Eq
| C_Reflect l1, C_Reflect l2 -> compare_name l1 l2
| C_Unit, _ -> Lt
| _, C_Unit -> Gt
| C_Int _, _ -> Lt
| _, C_Int _ -> Gt
| C_True, _ -> Lt
| _, C_True -> Gt
| C_False, _ -> Lt
| _, C_False -> Gt
| C_String _, _ -> Lt
| _, C_String _ -> Gt
| C_Range _, _ -> Lt
| _, C_Range _ -> Gt
| C_Reify, _ -> Lt
| _, C_Reify -> Gt
| C_Reflect _, _ -> Lt
| _, C_Reflect _ -> Gt