Skip to content

Instantly share code, notes, and snippets.



Last active Nov 15, 2017
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
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}
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