Lines Matching defs:compare
190 (case String.compare (s1,s2)
191 of EQUAL => Type.compare (ty1,ty2)
204 fun compare (p as (t1,t2)) =
207 (t1 as Clos _, t2) => compare (push_clos t1, t2)
208 | (t1, t2 as Clos _) => compare (t1, push_clos t2)
212 | (Bv i, Bv j) => Int.compare (i,j)
218 of EQUAL => Type.compare (to_hol_type ty1,
222 | (Comb(M,N),Comb(P,Q)) => (case compare (M,P)
223 of EQUAL => compare (N,Q)
228 Abs(Fv(_, ty2),N)) => (case Type.compare(ty1,ty2)
229 of EQUAL => compare (M,N)
233 val empty_tmset = HOLset.empty compare
234 fun term_eq t1 t2 = compare(t1,t2) = EQUAL
574 val emptysubst:(term,term)Binarymap.dict = Binarymap.mkDict compare
657 val varmap0 = mkDict compare
741 val AV = Uref.new (Redblackmap.mkDict String.compare) : ((string,occtype)Redblackmap.dict) Uref.t