8 files changed, 30 insertions(+), 21 deletions(-)

M Common.agda
M DFA.agda
M FA-Regex-Equiv.agda
M Fin.agda
M Lang.agda
M NFA.agda
M PFA.agda
M Regex.agda

@@ 11,3 11,17 @@ private
 
 it : {{_ : A}} → A
 it {{x}} = x
+
+infixr 0 _$_
+
+_$_
+  : ∀ {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁} {B : A → Type ℓ₂}
+  → ((x : A) → B x)
+  →  (x : A) → B x
+f $ x = f x
+
+_∋_ : ∀ {ℓ} (A : Type ℓ) → A → A
+A ∋ t = t
+
+postulate
+  TODO : A

@@ 21,17 21,6 @@ open import Common
 open import Lang
 open import Fin
 
-infixr 0 _$_
-
-_$_
-  : ∀ {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁} {B : A → Type ℓ₂}
-  → ((x : A) → B x)
-  →  (x : A) → B x
-f $ x = f x
-
-_∋_ : ∀ {ℓ} (A : Type ℓ) → A → A
-A ∋ t = t
-
 module _ (A : Type₀) {{isFinSetA : isFinSet A}} where
   record DFA : Type₁ where
     field

@@ 5,6 5,7 @@ module FA-Regex-Equiv where
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Logic
 
+open import Common
 open import Fin
 open import Lang
 open import DFA


@@ 14,10 15,10 @@ open import Regex
 
 module _ {A : Type₀} {{isFinSetA : isFinSet A}} where
   DFA~Regex : DfaLangs A ≡ RegexLangs A
-  DFA~Regex = {!!}
+  DFA~Regex = TODO
 
   DFA~NFA : DfaLangs A ≡ NfaLangs A
-  DFA~NFA = {!!}
+  DFA~NFA = TODO
 
   DFA~NFA-ε : DfaLangs A ≡ NFAεLangs A
-  DFA~NFA-ε = {!!}
+  DFA~NFA-ε = TODO

@@ 24,6 24,8 @@ open import Data.Fin using (Fin; zero; suc) public
 import Data.Fin.Properties
 import Data.Empty as Empty
 
+open import Common
+
 znots-std : ∀ {m} {n : Fin m} → zero ≡ suc n → [ ⊥ ]
 znots-std {m} {n} p = subst F p tt
   where


@@ 81,7 83,7 @@ FinSet = TypeWithStr _ isFinSet
 
 -- Is this even true?
 isFinSet→isSet : {{_ : isFinSet A}} → isSet A
-isFinSet→isSet = {!!}
+isFinSet→isSet = TODO
 
 instance
   isFinSetFin : ∀ {n} → isFinSet (Fin n)

@@ 11,6 11,7 @@ open import Cubical.Data.Empty renaming (⊥ to Empty)
 
 module Lang where
 
+open import Common
 open import Fin
 
 module _ {ℓ}{X : Type ℓ} where


@@ 55,10 56,10 @@ module _ (A : Type₀) {{isFinSetA : isFinSet A}} where
   ⟦ε⟧ = _^_ 0
 
   _ : _^* ≡ ⋃ ℕ (_^_)
-  _ = {!!}
+  _ = {!TODO!}
 
   _ : _^+ ≡ ⋃ ℕ (_^_ ∘ suc)
-  _ = {!!}
+  _ = TODO
 
   _ : _^* ≡ _^+ ∪ ⟦ε⟧
-  _ = {!!}
+  _ = TODO

@@ 69,4 69,4 @@ module example-2-6 where
   P (suc zero ∷ b ∷ w) = P (b ∷ w)
 
   _ : L ≡ P
-  _ = {!!}
+  _ = {!TODO!}

@@ 10,6 10,7 @@ open import Cubical.Data.List hiding ([_])
 open import Cubical.Data.Maybe
 open import Cubical.Data.Prod
 
+open import Common
 open import Lang
 open import Fin
 


@@ 92,7 93,7 @@ module _ (A : Type₀) {{isFinSetA : isFinSet A}} where
   EmptyStackPfaLangs N = ∃[ M ∶ PFA ] (empty-stack-lang M ≡ N) , powersets-are-sets _ _
 
   _ : FinalStatePfaLangs ≡ EmptyStackPfaLangs
-  _ = {!!}
+  _ = {!TODO!}
 
   {-
   Languages definable by pushdown finite automata

@@ 10,6 10,7 @@ open import Cubical.Data.Nat hiding (_+_; +-comm)
 open import Cubical.Data.List hiding ([_])
 open import Cubical.Data.List.Properties
 
+open import Common
 open import Lang hiding (∅)
 open import Fin
 


@@ 79,4 80,4 @@ module example where
   L = lang A x
 
   _ : L ≡ P
-  _ = {!!}
+  _ = TODO