Lines Matching refs:vis
185 return [vis for vis in self.pcs
186 if vis[0] != 'Bool']
188 return [vis for (_, vis) in self.vals]
282 def true_if_at_hyp (expr, vis, induct = None):
283 check_vis_is_vis (vis)
284 return Hyp ('EqIfAt', (expr, vis), (true_term, vis),
287 def pc_true_hyp (vis):
288 check_vis_is_vis (vis)
289 return Hyp ('PCImp', ('Bool', true_term), vis)
291 def pc_false_hyp (vis):
292 check_vis_is_vis (vis)
293 return Hyp ('PCImp', vis, ('Bool', false_term))
295 def pc_triv_hyp (vis):
296 check_vis_is_vis (vis)
297 return Hyp ('PCImp', vis, vis)