Lines Matching refs:depth
187 fun set_prove_depth db depth vgoal =
188 meson_prove_reduce_depth db (set_meson_frule db) depth vgoal;
313 fun subtype_check ccache congs stricttypechecking depth =
320 ((tm, depth), fn () => basic_subtypes facts tm)
363 val pre_results = set_prove_depth facts'' depth (before_vars, goal)
373 fun SUBTYPE_CHECK stricttypechecking depth sc tm =
375 stricttypechecking depth (subtype_context_facts sc) tm;
405 fun SUBTYPE_MATCH depth sc (vars, goal) =
408 val subtypes = SUBTYPE_CHECK false depth sc elt
410 val res = set_prove_depth facts depth (vars, goal)
415 fun SUBTYPE_PROVE depth sc goal =
416 (case SUBTYPE_MATCH depth sc (empty_vars, goal) of (_, (_, th)) :: _ => th
419 fun SUBTYPE_CONV_DEPTH depth sc goal = EQT_INTRO (SUBTYPE_PROVE depth sc goal);