Searched refs:Hyp (Results 1 - 4 of 4) sorted by last modified time

/seL4-l4v-10.1.1/graph-refine/
H A Drep_graph.py137 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 Dloop_bounds.py2 from rep_graph import vc_num, vc_offs, pc_true_hyp, Hyp, eq_hyp namespace
H A Dcheck.py11 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 DTactical.sml332 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