Lines Matching defs:dst
764 fun not_in_asserts p (dst: term -> term) =
768 val d = dst x
770 not (Lib.exists (fn y => case Lib.total dst y of
785 val (tm, mk, dst:term -> term * term, _:term -> bool) = syntax2 c
787 val c = fst o dst
1228 fun split_cond pre dst th =
1232 case List.mapPartial (Lib.total dst) p of
1319 group_into_chunks (dst, n, mk, is_big_end) l
1324 dst - identifies the access, e.g. arm_MEM
1381 fun group_into_chunks (dst, n, be) =
1383 group_into_n n o List.mapPartial (Lib.total dst)
1416 val (dst, n, _) = chunk_for m_def
1417 val dst = fst o dst
1422 val l = List.filter (Lib.can dst) (progSyntax.strip_star p)
1427 val base = dst (hd l)
1440 (boolSyntax.mk_eq (dst tm, mk (i, j))))
1462 val (dst, n, _) = chunk_for m_def
1463 val chunks = group_into_chunks (dst, n, be)
1530 val (dst, n, m_tm) = chunk_for m_def
1531 val chunks = group_into_chunks (dst, n, be)