Skip to content

Instantly share code, notes, and snippets.

@gergoerdi

gergoerdi/NumFin.agda

Last active Nov 15, 2017
Embed
What would you like to do?
open import Agda.Builtin.FromNat
open import Data.Fin
open import Relation.Nullary
open import Relation.Nullary.Decidable
open import Data.Nat renaming (_≤?_ to _N≤?_)
open import Data.Unit
instance
NumFin : {n} Number (Fin n)
Number.Constraint (NumFin {n}) k = True (suc k N≤? n)
Number.fromNat NumFin m {{m<n}}= #_ m {m<n = m<n}
instance
NumNat : Number ℕ
Number.Constraint NumNat _ =
Number.fromNat NumNat m = m
data I'mFinnish : Set where
Mk : Fin 5 I'mFinnish
foo : I'mFinnish
foo = Mk (# 3)
open import Data.Bool
-- This fails with
-- suc is not a constructor of the datatype Fin
-- when checking that the pattern suc (suc (suc zero)) has type Fin (fromNat 5)
bar′ : I'mFinnish Bool
bar′ (Mk 3) = true
bar′ _ = false
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.