Mercurial > hg > Members > kono > Proof > automaton
diff automaton-in-agda/src/lang-text.agda @ 405:af8f630b7e60
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 24 Sep 2023 18:02:04 +0900 |
| parents | 3fa72793620b |
| children |
line wrap: on
line diff
--- a/automaton-in-agda/src/lang-text.agda Sun Sep 24 13:20:31 2023 +0900 +++ b/automaton-in-agda/src/lang-text.agda Sun Sep 24 18:02:04 2023 +0900 @@ -3,7 +3,7 @@ open import Data.List open import Data.String open import Data.Char -open import Data.Char.Unsafe +-- open import Data.Char.Unsafe open import Relation.Binary.PropositionalEquality open import Relation.Nullary open import logic @@ -36,19 +36,19 @@ ex15c : Set -- w is any string not in a*b* -ex15c = (w : String ) → ( ¬ (contains w "ab" ≡ true ) /\ ( ¬ (contains w "ba" ≡ true ) +ex15c = (w : String ) → ( ¬ (contains w "ab" ≡ true )) /\ ( ¬ (contains w "ba" ≡ true ) ) -ex15d : {!!} -ex15d = {!!} +ex15d : ? +ex15d = ? -ex15e : {!!} -ex15e = {!!} +ex15e : ? +ex15e = ? -ex15f : {!!} -ex15f = {!!} +ex15f : ? +ex15f = ? -ex15g : {!!} -ex15g = {!!} +ex15g : ? +ex15g = ? -ex15h : {!!} -ex15h = {!!} +ex15h : ? +ex15h = ?