12345678910111213141516171819202122232425-------------------------------------------------------------------------- The Agda standard library---- Patterns for Fin------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} module Data.Fin.Patterns where open import Data.Fin.Base -------------------------------------------------------------------------- Constants pattern 0F = zeropattern 1F = suc 0Fpattern 2F = suc 1Fpattern 3F = suc 2Fpattern 4F = suc 3Fpattern 5F = suc 4Fpattern 6F = suc 5Fpattern 7F = suc 6Fpattern 8F = suc 7Fpattern 9F = suc 8F