Lines Matching refs:check
76 "Bounded rewrites branch, and bypass permutative loop check"
98 fun check (th1, th2) =
103 "Bounded rewrites override mk_rewrites loop check"
104 check
115 fun check th = aconv (rhs (concl th)) ``f (x:'a):'a = z``
119 check
130 fun check th = not (aconv (rhs (concl th)) ``x:bool``)
134 check
145 fun check th = aconv (rhs (concl th)) result
147 infloop_protect "Congruence for conditional expressions" check doit t
156 fun check th = aconv (rhs (concl th)) result
158 infloop_protect "SimpL on operator returning non-boolean" check doit t
167 fun check th = aconv (rhs (concl th)) result
169 infloop_protect "Satisfy" check doit t
181 fun check (sgs, vfn) = let
190 infloop_protect "Abbrev-simplification with abstraction" check doit g
200 fun check th = th |> concl |> rhs |> aconv F
202 infloop_protect "assume T=F and F=T (if hangs, it's failed)" check doit t
210 fun check th = th |> concl |> rhs |> aconv F
212 infloop_protect "CONJ_ss with T=F and F=T assumptions (if hangs, it's failed)" check doit t