[ base ] Implement Uninhabited for impossible Pointwise equalities

CHANGELOG.md

@@ -135,6 +135,7 @@
   which takes a witness of `finToNat k = finToNat l` and proves `k ~~~ l`.
 * Drop first argument (path to the `node` executable) from `System.getArgs` on
   the Node.js backend to make it consistent with other backends.
+* Adds `Uninhabited` instances for `FZ ~~~ FS k` and `FS k ~~~ FZ`.
 
 #### Test
 

libs/base/Data/Fin.idr

@@ -304,6 +304,16 @@ namespace Equality
   (~~~) : Fin m -> Fin n -> Type
   (~~~) = Pointwise
 
+  export
+  Uninhabited (FS k ~~~ FZ) where
+    uninhabited FZ impossible
+    uninhabited (FS _) impossible
+
+  export
+  Uninhabited (FZ ~~~ FS k) where
+    uninhabited FZ impossible
+    uninhabited (FS _) impossible
+
   ||| Pointwise equality is reflexive
   export
   reflexive : {k : Fin m} -> k ~~~ k