pattern-matching - 在 Fin 模式中使用文字数字

Question

一方面，我可以使用从文字#_构造s ：Fin

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

我的问题是，我可以在紧握的手上Fin匹配s时使用文字吗？即，我可以做些什么来近似以下无效的 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.