Searched refs:ProofNode (Results 1 - 3 of 3) sorted by relevance

/seL4-l4v-master/graph-refine/
H A Dcheck.py154 class ProofNode: class in inherits:
179 return 'ProofNode (%r, %r, %r)' % (self.kind,
272 return (i + 1, ProofNode ('Leaf'))
281 return (i, ProofNode ('Restr', (point, (kind, (x, y))), [p1]))
290 return (i, ProofNode ('SingleRevInduct', (point, (eqs, n),
300 return (i, ProofNode ('Split', (l_details, r_details, eqs,
307 return (i, ProofNode ('CaseSplit', (n, tag), [p1, p2]))
H A Dstats.py11 from check import ProofNode namespace
29 if line.startswith ('ProofNode '):
H A Dsearch.py10 from check import restr_others, loops_to_split, ProofNode namespace
1714 return ProofNode ('Leaf', None, ())
1740 return ProofNode (kind, details, subpfs)
1776 return ProofNode ('Restr', (sp, (kind, (min_v, max_v))), [subproof])

Completed in 43 milliseconds