Lines Matching refs:depth
307 type state = {env : subst, depth : int, proof : thm list, offset : int};
309 fun update_env f ({env, depth, proof, offset} : state) =
310 {env = f env, depth = depth, proof = proof, offset = offset};
312 fun update_depth f ({env, depth, proof, offset} : state) =
313 {env = env, depth = f depth, proof = proof, offset = offset};
315 fun update_proof f ({env, depth, proof, offset} : state) =
316 {env = env, depth = depth, proof = f proof, offset = offset};
318 fun update_offset f ({env, depth, proof, offset} : state) =
319 {env = env, depth = depth, proof = proof, offset = f offset};
356 fun purify (s as {env, depth = n, ...} : state) =
427 fun spend m f c (s as {depth = n, ...} : state) =
431 fun check (s' as {depth = n', ...} : state) =
491 and expand_rule ancestors g cont {env, depth, proof, offset} r () =
494 val depth = depth - #asmn r
496 if 0 <= depth then ()
505 {env = env, depth = depth, proof = proof, offset = offset}
507 and expands ancestors g c (s as {depth = n, ...}) =
543 fun raw_meson system goals depth =
547 {env = |<>|, depth = depth, proof = [], offset = 0});