Mercurial > hg > Members > kono > Proof > automaton

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

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 24 Sep 2023 18:02:04 +0900
parents a5c874396cc4
children 207e6c4e155c
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 module regex where 4 module regex where
3 5
4 open import Level renaming ( suc to succ ; zero to Zero ) 6 open import Level renaming ( suc to succ ; zero to Zero )
5 open import Data.Fin hiding ( pred ) 7 open import Data.Fin hiding ( pred )
6 open import Data.Nat hiding ( _≟_ ) 8 open import Data.Nat hiding ( _≟_ )