val compare_universes (us1 us2: universes) : order
let compare_universes (us1 us2:universes) : order =
  compare_list us1 us2 compare_universe
val compare_universes (us1 us2: universes) : order
let compare_universes (us1 us2: universes) : order =
compare_list us1 us2 compare_universe
FStar.Reflection.V1.Compare.fst.checked
prims.fst.checked FStar.Reflection.V1.Derived.fst.checked FStar.Reflection.V1.Data.fsti.checked FStar.Reflection.V1.Builtins.fsti.checked FStar.Reflection.Types.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Order.fst.checked
FStar.Reflection.V1.Compare.fst
FStar.Reflection.V1.Data.universes FStar.Order.compare_list FStar.Reflection.Types.universe FStar.Reflection.V1.Compare.compare_universe FStar.Order.order
(*
   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.Reflection.Types
open FStar.Reflection.V1.Data
open FStar.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)

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

let compare_binder (b1 b2 : binder) : order =
    let bview1 = inspect_binder b1 in
    let bview2 = inspect_binder b2 in
    compare_bv bview1.binder_bv bview2.binder_bv

let compare_ident (i1 i2:ident) : order =
  order_from_int (compare_string (fst i1) (fst i2))

let rec compare_universe (u1 u2:universe) : order =
  match inspect_universe u1, inspect_universe u2 with
  | Uv_Zero, Uv_Zero -> Eq
  | Uv_Succ u1, Uv_Succ u2 -> compare_universe u1 u2
  | Uv_Max us1, Uv_Max us2 ->
    compare_list us1 us2 (fun x y -> compare_universe x y)
  | Uv_BVar n1, Uv_BVar n2 -> compare_int n1 n2
  | Uv_Name i1, Uv_Name i2 -> compare_ident i1 i2
  | Uv_Unif u1, Uv_Unif u2 -> Eq  //AR: TODO
  | Uv_Unk, Uv_Unk -> Eq
  | Uv_Zero, _ -> Lt | _, Uv_Zero -> Gt
  | Uv_Succ _, _ -> Lt | _, Uv_Succ _ -> Gt
  | Uv_Max _, _ -> Lt | _, Uv_Max _ -> Gt
  | Uv_BVar _, _ -> Lt | _, Uv_BVar _ -> Gt
  | Uv_Name _, _ -> Lt | _, Uv_Name _ -> Gt
  | Uv_Unif _, _ -> Lt | _, Uv_Unif _ -> Gt
  | Uv_Unk, _ -> Lt
val compare_universes (us1 us2: universes) : order
us1: FStar.Reflection.V1.Data.universes -> us2: FStar.Reflection.V1.Data.universes
  -> FStar.Order.order