val test1 : _: Prims.unit -> Prims.unit
let test1 () = assert_norm (calc_chain_compatible [(<); (<=)] (<))
module BasicTests

open FStar.Preorder
open FStar.Calc

(* Ouch, (>=) doesn't typecheck as a preorder *)
let (<=) : relation int = (fun x y -> x <= y <: Type)
let (>=) : relation int = (fun x y -> x >= y <: Type)
let (>) : relation int = (fun x y -> x > y <: Type)
let (<) : relation int = (fun x y -> x < y <: Type)
/
prims.fst.checked FStar.Preorder.fst.checked FStar.Pervasives.fsti.checked FStar.Calc.fsti.checked
BasicTests.fst
_: Prims.unit -> Prims.unit
Prims.unit FStar.Pervasives.assert_norm FStar.Calc.calc_chain_compatible Prims.int Prims.Cons FStar.Preorder.relation BasicTests.op_Less BasicTests.op_Less_Equals Prims.Nil
let test1 () =
  
assert_norm (calc_chain_compatible [( < ); ( <= )] ( < ))