Stuff for automata (DFA, NFA, ε-NFA) written in Idris.
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

Main.idr 601B

1234567891011121314151617181920212223242526272829303132
  1. module Main
  2. import Data.Automata
  3. import Data.Fin
  4. import Data.Listable
  5. nenTuples : List (Fin 4, Fin 2, Fin 4)
  6. nenTuples = [(0, 0, 1), (0, 1, 0), (1, 0, 1), (1, 1, 2), (2, 0, 3), (2, 1, 0), (3, 0, 3), (3, 1, 3)]
  7. nen : DFA (Fin 4) (Fin 2)
  8. nen = MkDFA (toDeltaDFA nenTuples) 0 [3]
  9. testInput1 : List (Fin 2)
  10. testInput1 = [0,1,1,0,1,1,0,1]
  11. interface ListableType (t : Type) where
  12. listed : List t
  13. -- ListableType (Fin n) where
  14. -- listed = n :: lk where
  15. -- lk : Fin (n - 1)
  16. -- lk = listed
  17. {-
  18. l1 : List (Fin 1)
  19. l1 = listed-}
  20. drei : Nat
  21. drei = 3
  22. testlel : Nat
  23. testlel = testkek