comparison automaton-in-agda/src/regex2.agda @ 405:af8f630b7e60

...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 24 Sep 2023 18:02:04 +0900
parents a5c874396cc4
children
comparison
equal deleted inserted replaced
404:dfaf230f7b9a 405:af8f630b7e60
1 {-# OPTIONS --allow-unsolved-metas #-} 1 {-# OPTIONS --cubical-compatible --safe #-}
2
3 -- {-# OPTIONS --allow-unsolved-metas #-}
2 4
3 open import Relation.Binary.PropositionalEquality hiding ( [_] ) 5 open import Relation.Binary.PropositionalEquality hiding ( [_] )
4 open import Relation.Nullary using (¬_; Dec; yes; no) 6 open import Relation.Nullary using (¬_; Dec; yes; no)
5 open import Data.List hiding ( [_] ) 7 open import Data.List hiding ( [_] )
6 open import Data.Empty 8 open import Data.Empty