Lines Matching defs:syntax
10 from syntax import (true_term, false_term, boolT, mk_and, mk_not, mk_implies,
12 import syntax
257 return syntax.true_term
259 return syntax.false_term
265 return syntax.mk_n_implies ([x_pc, y_pc], eq)
449 imp = syntax.mk_implies (pc, prev_pc_env[0])
622 if typ == syntax.builtinTs['Mem']:
901 if typ == syntax.builtinTs['Mem']]
1072 return logic.strengthen_hyp (syntax.mk_n_implies (hyps, concl))
1139 return syntax.adjust_op_vals (expr, vals)
1146 if x.typ == syntax.builtinTs['RelWrapper']:
1197 if typ == syntax.builtinTs['Mem']]:
1249 args = [syntax.mk_var (nm, typ) for (nm, typ) in args]
1257 if x.typ.kind == 'Word' or x.typ == syntax.builtinTs['Mem']