Skip to content

Instantly share code, notes, and snippets.

@mietek

mietek/subttle.agda Secret

Created April 13, 2017 06:38
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save mietek/bb5e152660c12abf1b59a69aab5d4f0f to your computer and use it in GitHub Desktop.
Save mietek/bb5e152660c12abf1b59a69aab5d4f0f to your computer and use it in GitHub Desktop.
Download ZIP
Raw
subttle.agda
module subttle where
open import Data.Nat
open import Data.Fin
open import Relation.Binary.PropositionalEquality
minFin : ∀ {n} → Fin (suc n)
minFin = zero
maxFin : ∀ {n} → Fin (suc n)
maxFin {zero} = zero
maxFin {suc n} = suc maxFin
minFin≡0 : ∀ {n} → minFin {n} ≡ zero
minFin≡0 = refl
maxFin≡n : ∀ {n} → maxFin {n} ≡ fromℕ n
maxFin≡n {zero} = refl
maxFin≡n {suc n} = cong suc maxFin≡n
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment