blob: 2416e3ad1344b4ec92b33012ddb0dab31b3b8c88 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
|
Set Uniform Inductive Parameters.
Inductive test (X : Set) : Prop :=
with test2 (X : Set) : X -> Prop :=
| C (x : X) : test2 x.
Require Import List.
Import ListNotations.
Set Suggest Proof Using.
Set Primitive Projections.
Section Grammar.
Variable A : Type.
Record grammar : Type := Grammar {
gm_nonterm :> Type ;
gm_rules :> list (gm_nonterm * list (A + gm_nonterm)) ;
}.
Set Uniform Inductive Parameters.
Inductive lang (gm : grammar) : gm -> list A -> Prop :=
| lang_rule S ps ws : In (S, ps) gm -> lmatch ps ws -> lang S (concat ws)
with lmatch (gm : grammar) : list (A + gm) -> list (list A) -> Prop :=
| lmatch_nil : lmatch [] []
| lmatch_consL ps ws a : lmatch ps ws -> lmatch (inl a :: ps) ([a] :: ws)
| lmatch_consR ps ws S w :
lang S w -> lmatch ps ws -> lmatch (inr S :: ps) (w :: ws)
.
End Grammar.
|
