Используйте буквенные числа в шаблонах Fin

Question

С одной стороны, я могу использовать #_ строить Fins из литералов:

open import Data.Fin

data I'mFinnish : Set where
  Mk : Fin 5 → I'mFinnish

foo : I'mFinnish
foo = Mk (# 3)

С другой стороны, я могу использовать литералы для сопоставления с образцом на натуральных объектах:

open import Data.Nat

data I'mANatural : Set where
  Mk : ℕ → I'mANatural

open import Data.Bool
bar : I'mANatural → Bool
bar (Mk 3) = true
bar _      = false

Мой вопрос, могу ли я, сжимая руку, использовать литералы при сопоставлении на Fins? То есть, что я могу сделать, чтобы приблизить следующий, неверный, как есть, код Agda:

open import Data.Bool
bar′ : I'mFinnish → Bool
bar′ (Mk 3) = true
bar′ _      = false

Answer 1

Вы ищете буквальную перегрузку. Цитируя документацию, модуль Agda.Builtin.FromNat предоставляет класс типов

record Number {a} (A : Set a) : Set (lsuc a) where
  field
    Constraint : Nat → Set a
    fromNat : ∀ n → {{_ : Constraint n}} → A

open Number {{...}} public using (fromNat)

{-# BUILTIN FROMNAT fromNat #-}

что позволяет перегружать природные литералы. Экземпляр для Fin можно найти и по предыдущей ссылке. И вы можете напрямую определить экземпляр для I'mFinnish,