rampion · May 18, 2017 02:25 · May 18, 2017
diff --git a/FIn.hs b/FIn.hs
@@ -0,0 +1,26 @@
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE ViewPatterns #-}
+module Fin where
+
+data Nat = Z | S Nat
+
+newtype Fin (n :: Nat) = Fin { unFin :: Int }
+
+pattern FZ :: Fin ('S n)
+pattern FZ = Fin 0
+
+pattern FS :: Fin n -> Fin ('S n)
+pattern FS f <- (finPred -> Just f)
+  where FS = finSucc
+
+finPred :: Fin ('S n) -> Maybe (Fin n)
+finPred (Fin 0) = Nothing
+finPred (Fin i) = Just (Fin (pred i))
+
+finSucc :: Fin n -> Fin ('S n)
+finSucc (Fin i) = Fin (succ i)
+
+x :: Int
+x = case FZ of { FS (Fin i) -> i ; _ -> 1 }