Lines Matching refs:seq
19 | seq of pegsym => pegsym => ('c -> 'c -> 'c)
45 (���e1 e2 s f. peg_eval G (s, e1) NONE ��� peg_eval G (s, seq e1 e2 f) NONE) ���
48 peg_eval G (s0, seq e1 e2 f) NONE) ���
52 peg_eval G (s0, seq e1 e2 f) (SOME(s2, f c1 c2))) ���
135 (* seq rules *)
138 pegfail G (seq e1 e2 f)) ���
141 peggt0 G (seq e1 e2 f)) ���
142 (���e1 e2 f. peg0 G e1 ��� peg0 G e2 ��� peg0 G (seq e1 e2 f)) ���
215 wfpeg G (seq e1 e2 f)) ���
226 (subexprs (seq e1 e2 f3) = seq e1 e2 f3 INSERT subexprs e1 ��� subexprs e2) ���
265 (seq e1 e2 f ��� Gexprs G ��� e1 ��� Gexprs G ��� e2 ��� Gexprs G) ���
307 >- ((* seq *) Q.MATCH_ASSUM_ABBREV_TAC `seq e1 e2 f ��� Gexprs G` >>
332 val pegf_def = Define`pegf sym f = seq sym (empty ARB) (��l1 l2. f l1)`
335 ignoreL s1 s2 = seq s1 s2 (��a b. b)
341 ignoreR s1 s2 = seq s1 s2 (��a b. a)
357 ``peg_eval G (i0, seq s1 s2 f) (SOME (i,r)) ���
364 ``peg_eval G (i0, seq s1 s2 f) NONE ���
459 ``peg0 G (seq s1 s2 f) ��� peg0 G s1 ��� peg0 G s2``,