Lines Matching defs:expected
243 val expected = let
257 SOME ([([],subgoal)],_) => if aconv subgoal expected then OK()
416 fun tpp (s,expected) = let
421 if res = expected then OK()
422 else die (testutils.clear (" Expected >" ^ expected ^ "<; got >"^res^"<"))
594 val expected = mk_conj(mk_comb(I, p), mk_comb(I, q))
596 if aconv (rhs (concl result)) expected then OK()
604 val expected = lmk(List.tabulate(3, B))
615 if aconv expected res then OK()
751 val expected = ``?y:'a. (a = y) /\ (y = b)``
755 [([], sg)] => if aconv sg expected then OK() else die ""
876 val expected = ``Q (y:'a) (f (ARB:'b) : 'c) : bool``
881 EQUAL => if aconv expected g' then OK()
883 "; expected "^term_to_string expected)
905 "; expected " ^ term_to_string expectedg)
929 "; expected " ^ term_to_string expectedg)
948 "; expected " ^ term_to_string expectedg)
968 "; expected " ^ term_to_string expectedg)
988 "; expected " ^ term_to_string expectedg)
1009 "; expected " ^ term_to_string expectedg)
1031 "; expected " ^ term_to_string expectedg)
1061 "; expected " ^ term_to_string expectedg)
1103 "; expected " ^ term_to_string expectedg)
1124 "; expected " ^ term_to_string expectedg)
1139 fun test (nm, pat, expected) =
1144 require (check_result (equal expected))