From 3755a31bee638aeb4798705e62e76d88e15d7247 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Sat, 19 Aug 2023 14:22:40 -0700
Subject: [PATCH] Remove the starter files in NatMap

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 NatMap.agda | 56 -----------------------------------------------------
 1 file changed, 56 deletions(-)
 delete mode 100644 NatMap.agda

diff --git a/NatMap.agda b/NatMap.agda
deleted file mode 100644
index 0df05ba..0000000
--- a/NatMap.agda
+++ /dev/null
@@ -1,56 +0,0 @@
-module NatMap where
-
-open import Agda.Primitive using (Level)
-open import Data.Nat using (ℕ; _<?_; _≟_)
-open import Data.Nat.Properties using (<-cmp)
-open import Data.String using (String; _++_)
-open import Data.List using (List; []; _∷_)
-open import Data.Product using (_×_; _,_)
-open import Relation.Nullary using (yes; no)
-open import Relation.Binary using (Tri)
-open import Agda.Builtin.Equality using (_≡_; refl)
-
-variable
-    a : Level
-    A : Set a
-
--- It's easiest to reason about a linear-insertion map.
-
-NatMap : (A : Set a) → Set a
-NatMap A = List (ℕ × A)
-
-insert : ℕ → A → NatMap A -> NatMap A
-insert n a [] = (n , a) ∷ []
-insert n a l@(x@(n' , a') ∷ xs) with n <? n'
-...                             | yes n≡n' = (n , a) ∷ l
-...                             | no n≢n' = x ∷ insert n a xs
-
-
-testInsert₁ : insert 3 "third" [] ≡ (3 , "third") ∷ []
-testInsert₁ = refl
-
-testInsert₂ : insert 4 "fourth" ((3 , "third") ∷ []) ≡ (3 , "third") ∷ (4 , "fourth") ∷ []
-testInsert₂ = refl
-
-testInsert₃ : insert 2 "second" ((3 , "third") ∷ (4 , "fourth") ∷ []) ≡ (2 , "second") ∷ (3 , "third") ∷ (4 , "fourth") ∷ []
-testInsert₃ = refl
-
-{-# TERMINATING #-}
-merge : (A -> A -> A) -> NatMap A -> NatMap A -> NatMap A
-merge _ [] m₂ = m₂
-merge _ m₁ [] = m₁
-merge f m₁@(x₁@(n₁ , a₁) ∷ xs₁) m₂@(x₂@(n₂ , a₂) ∷ xs₂) with <-cmp n₁ n₂
-...                                                     | Tri.tri< _ _ _ = x₁ ∷ merge f xs₁ m₂
-...                                                     | Tri.tri> _ _ _ = x₂ ∷ merge f m₁ xs₂
-...                                                     | Tri.tri≈ _ _ _ = (n₁ , f a₁ a₂) ∷ merge f xs₁ xs₂
-
-testMerge : merge (_++_) ((1 , "one") ∷ (2 , "two") ∷ []) ((2 , "two") ∷ (3 , "three") ∷ []) ≡ (1 , "one") ∷ (2 , "twotwo") ∷ (3 , "three") ∷ []
-testMerge = refl
-
--- Note to self: will it be tricky to define a Semilattice instance for this?
---               I'm worried because proofs will likely require knowing the ordering -- merge certainly relies on it, but
---               we can't prove commutativity if the NatMap type includes a proof of ordering, because then we'll need
---               to compare `<=` for equality, which are going to be defined in terms of `=`...
---
---               We might need to generalize Lattice and friends to use ≈. But then,
---               pain in the ass for products because they'll need to lift ≈ ...