refactor: add erasure to So

Author: 4e554c4c

src/Data/Bool/Base.lagda.md

@@ -81,8 +81,9 @@ is-true true  = ⊤
 is-true false = ⊥
 
 record So (b : Bool) : Type where
+  constructor evidently
   field
-    is-so : is-true b
+    .{is-so} : is-true b
 
 pattern oh = record { is-so = tt }
 ```
@@ -104,7 +105,7 @@ instance
   H-Level-So : ∀ {x n} → H-Level (So x) (suc n)
   H-Level-So {false} = prop-instance λ ()
   H-Level-So {true} = prop-instance λ where
-    oh oh → refl
+    _ _ → refl
 
   Dec-So : ∀ {x} → Dec (So x)
   Dec-So = oh? _

src/Data/List/Base.lagda.md

@@ -348,11 +348,8 @@ _!?_ : List A → Nat → Maybe A
 
 -- Make sure that all of the actual computation is guarded behind irrelevance to make this zero cost
 !?-just : ∀ (xs : List A) (n : Nat) → .(n Nat.< length xs) → is-just (xs !? n)
-!?-just {A = a} xs n n<xs = erase (worker xs n n<xs)
-  where
-    worker : ∀ (xs : List A) (n : Nat) → n Nat.< length xs → is-true (is-just? (xs !? n))
-    worker (x ∷ xs) zero n<xs = tt
-    worker (x ∷ xs) (suc n) n<xs = worker xs n (Nat.≤-peel n<xs)
+!?-just {A = a} (x ∷ xs) zero n<xs = just-because evidently
+!?-just {A = a} (x ∷ xs) (suc n) n<xs = !?-just xs n (Nat.≤-peel n<xs)
 
 _!_ : (l : List A) → Fin (length l) → A
 xs ! (fin n ⦃ forget pf ⦄) = from-just! _ $ !?-just xs n pf

src/Data/Maybe/Base.lagda.md

@@ -89,9 +89,9 @@ is-just? nothing = false
 is-just? (just _) = true
 
 record is-just (m : Maybe A) : Type where
-  constructor erase
+  constructor just-because
   field
-    .witness : is-true (is-just? m)
+    witness : So (is-just? m)
 
 
 from-just! : ∀ x → is-just x → A