Mercurial > hg > Members > kono > Proof > automaton
comparison agda/regex.agda @ 9:e7bb980408fb
separate epsiron
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Wed, 22 Aug 2018 21:59:24 +0900 |
parents | cdf75ae6f0c1 |
children | 8e66865fd9af |
comparison
equal
deleted
inserted
replaced
8:cdf75ae6f0c1 | 9:e7bb980408fb |
---|---|
21 -- data In2 : Set where | 21 -- data In2 : Set where |
22 -- a : In2 | 22 -- a : In2 |
23 -- b : In2 | 23 -- b : In2 |
24 | 24 |
25 open import automaton | 25 open import automaton |
26 open import epautomaton | |
26 | 27 |
27 | 28 |
28 record RST ( Σ : Set ) | 29 record RST ( Σ : Set ) |
29 : Set where | 30 : Set where |
30 inductive | 31 inductive |