Searched refs:Hyp (Results 1 - 4 of 4) sorted by last modified time
/seL4-l4v-10.1.1/graph-refine/ |
H A D | rep_graph.py | 137 class Hyp: class in inherits: 163 return 'Hyp (%r, %s)' % (self.kind, ', '.join (vals)) 280 return Hyp (kind, lhs, rhs, induct = induct) 284 return Hyp ('EqIfAt', (expr, vis), (true_term, vis), 289 return Hyp ('PCImp', ('Bool', true_term), vis) 293 return Hyp ('PCImp', vis, ('Bool', false_term)) 297 return Hyp ('PCImp', vis, vis)
|
H A D | loop_bounds.py | 2 from rep_graph import vc_num, vc_offs, pc_true_hyp, Hyp, eq_hyp namespace
|
H A D | check.py | 11 from rep_graph import mk_graph_slice, Hyp, eq_hyp, pc_true_hyp, pc_false_hyp namespace 409 hyps = [(Hyp ('PCImp', l_visit, r_visit), 'pc imp'), 410 (Hyp ('PCImp', l_visit, l_start), '%s pc imp' % l_tag), 411 (Hyp ('PCImp', r_visit, r_start), '%s pc imp' % r_tag)] 584 hyps = [(Hyp ('PCImp', visit, start), '%s pc imp' % tag)]
|
/seL4-l4v-10.1.1/HOL4/src/1/ |
H A D | Tactical.sml | 332 datatype validity_failure = Concl of term | Hyp of term 338 | SOME h => SOME (Hyp h) 344 Hyp h => ("bad hypothesis", h)
|
Completed in 84 milliseconds