Lines Matching defs:pats
599 (* get pats with fresh vars to do a quick prefiltering *)
2208 (* COMPUTE CASE-DISTINCTION based on pats *)
2226 val pats = List.map (#1 o dest_PMATCH_ROW) rows
2231 val pats = [``\(x:num). 2``]
2232 val pats = [``\(x:num). [2;3;4]``]
2264 fun mk_initial_state var_gen lbl_gen pats = let
2265 val (_, p) = pairSyntax.dest_pabs (hd pats)
2269 val cols = dest_PATLIST_COLS initial_value pats
2416 fun nchotomy_of_pats_GEN db col_heu pats = let
2421 val (thm, cols, lbl) = mk_initial_state var_gen lbl_gen pats
2451 val thm3 = compile (mk_initial_state var_gen lbl_gen pats)
2459 fun nchotomy_of_pats pats =
2460 nchotomy_of_pats_GEN (!thePmatchCompileDB) colHeu_default pats
2508 val pats = List.map (#1 o dest_PMATCH_ROW) rows
2511 val thm = CONV_RULE (nchotomy2PMATCH_ROW_COND_EX_CONV) (nchotomy_of_pats pats)
2735 val pats = List.map (#1 o dest_PMATCH_ROW) rows
2736 val thm01 = nchotomy_of_pats_GEN db col_heu pats
3087 val pats = List.map (#2 o dest_PMATCH_ROW_COND_EX) disjs
3088 val thm01 = nchotomy_of_pats_GEN db col_heu pats