------------------------------------------------------------------------
-- The Agda standard library
--
-- Showing finite numbers
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Data.Fin.Show where
open import Data.Fin.Base using (Fin; toℕ; fromℕ<)
open import Data.Maybe.Base using (Maybe; nothing; just; _>>=_)
open import Data.Nat as ℕ using (ℕ; _≤?_; _<?_)
import Data.Nat.Show as ℕ using (show; readMaybe)
open import Data.String.Base using (String)
open import Function.Base
open import Relation.Nullary.Decidable using (yes; no)
open import Relation.Nullary.Decidable using (True)
show : ∀ {n} → Fin n → String
show = ℕ.show ∘′ toℕ
readMaybe : ∀ {n} base {base≤16 : True (base ≤? 16)} → String → Maybe (Fin n)
readMaybe {n} base {pr} str = do
nat ← ℕ.readMaybe base {pr} str
case nat <? n of λ where
(yes pr) → just (fromℕ< pr)
(no ¬pr) → nothing
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