------------------------------------------------------------------------
-- The Agda standard library
--
-- Patterns for Fin
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Data.Fin.Patterns where
open import Data.Fin.Base using (Fin; zero; suc)
------------------------------------------------------------------------
-- Constants
pattern 0F = zero
pattern 1F = suc 0F
pattern 2F = suc 1F
pattern 3F = suc 2F
pattern 4F = suc 3F
pattern 5F = suc 4F
pattern 6F = suc 5F
pattern 7F = suc 6F
pattern 8F = suc 7F
pattern 9F = suc 8F
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4