Mercurial > hg > Members > kono > Proof > automaton
diff agda/cfg.agda @ 46:964e4bd0272a
add coinduction
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 05 Apr 2019 16:13:44 +0900 |
| parents | 31e4bd173951 |
| children |
line wrap: on
line diff
--- a/agda/cfg.agda Sat Dec 22 15:48:05 2018 +0900 +++ b/agda/cfg.agda Fri Apr 05 16:13:44 2019 +0900 @@ -118,17 +118,17 @@ ( Token t:IF ∷ expr ∷ statement ∷ Token t:ELSE ∷ statement ∷ [] ) ∷ [] -cgftest1 = cfg-language IFGrammer ( t:SA ∷ [] ) +cfgtest1 = cfg-language IFGrammer ( t:SA ∷ [] ) -cgftest2 = cfg-language2 IFGrammer (Token t:SA) ( t:SA ∷ [] ) +cfgtest2 = cfg-language2 IFGrammer (Token t:SA) ( t:SA ∷ [] ) -cgftest3 = cfg-language1 IFGrammer (Token t:SA ∷ [] ) ( t:SA ∷ [] ) +cfgtest3 = cfg-language1 IFGrammer (Token t:SA ∷ [] ) ( t:SA ∷ [] ) -cgftest4 = cfg-language IFGrammer (t:IF ∷ t:EA ∷ t:SA ∷ [] ) +cfgtest4 = cfg-language IFGrammer (t:IF ∷ t:EA ∷ t:SA ∷ [] ) -cgftest5 = cfg-language1 IFGrammer (Token t:IF ∷ expr ∷ statement ∷ []) (t:IF ∷ t:EA ∷ t:EA ∷ [] ) -cgftest6 = cfg-language2 IFGrammer statement (t:IF ∷ t:EA ∷ t:SA ∷ [] ) -cgftest7 = cfg-language1 IFGrammer (Token t:IF ∷ expr ∷ statement ∷ Token t:ELSE ∷ statement ∷ []) (t:IF ∷ t:EA ∷ t:SA ∷ t:ELSE ∷ t:SB ∷ [] ) +cfgtest5 = cfg-language1 IFGrammer (Token t:IF ∷ expr ∷ statement ∷ []) (t:IF ∷ t:EA ∷ t:EA ∷ [] ) +cfgtest6 = cfg-language2 IFGrammer statement (t:IF ∷ t:EA ∷ t:SA ∷ [] ) +cfgtest7 = cfg-language1 IFGrammer (Token t:IF ∷ expr ∷ statement ∷ Token t:ELSE ∷ statement ∷ []) (t:IF ∷ t:EA ∷ t:SA ∷ t:ELSE ∷ t:SB ∷ [] ) -cgftest8 = cfg-language IFGrammer (t:IF ∷ t:EA ∷ t:IF ∷ t:EB ∷ t:SA ∷ t:ELSE ∷ t:SB ∷ [] ) +cfgtest8 = cfg-language IFGrammer (t:IF ∷ t:EA ∷ t:IF ∷ t:EB ∷ t:SA ∷ t:ELSE ∷ t:SB ∷ [] )