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