Searched refs:ProofNode (Results 1 - 3 of 3) sorted by relevance
/seL4-l4v-master/graph-refine/ |
H A D | check.py | 154 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 D | stats.py | 11 from check import ProofNode namespace 29 if line.startswith ('ProofNode '):
|
H A D | search.py | 10 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