Mercurial > hg > Members > kono > Proof > automaton

diff agda/regex.agda @ 11:8e66865fd9af

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix sbconst
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 24 Aug 2018 11:44:41 +0900
parents e7bb980408fb
children 02b4ecc9972c
line wrap: on
line diff
--- a/agda/regex.agda	Thu Aug 23 16:33:53 2018 +0900
+++ b/agda/regex.agda	Fri Aug 24 11:44:41 2018 +0900
@@ -117,11 +117,17 @@
        Rstates =  [ Rstart R ] ++ Rstates R 
      }
 
+In2toℕ : In2 → ℕ
+In2toℕ i1 = zero
+In2toℕ i2 = 1
+
+
 regex2nfa :  (regex : Regex In2 ) → εAutomaton (RST In2) In2 
 regex2nfa regex = record {
       εδ =  move 
     ; all-εδ =  cond1
     ; εid = λ s → state s
+    ; Σid = λ s → In2toℕ s
     ; allState = Rstates G
     ; εstart =   Rstart G
     ; εend = λ s → RSTend s }