主页 / coding / 问题 / 79420541
Accepted
dec
Asked: 2025-02-07 18:28:59 +0800 CST

Agda：有没有办法在函数定义中使用 with-abstraction 提供的信息？

  • 772

我正在尝试构建具有如下定义的数据类型的区间格：

data 𝕀 : Set where
  ⊤   : 𝕀
  ⊥   : 𝕀
  -∞  : ℤ → 𝕀
  _+∞ : ℤ → 𝕀
  I   : (l : ℤ) → (u : ℤ) → {l ≤ u} → 𝕀

为了在某​​些情况下在区间上定义 ⊓𝕀 (glb) 运算符，我必须进行模式匹配i ≤ᵇ j以定义运算符的适当值，尽管我不确定如何在案例定义中重用模式匹配提供的信息。

特别是在

-∞ x ⊓𝕀 (y +∞) with (y ≤ᵇ x) | inspect (y ≤ᵇ_) x
... | false | [ y≤x≡ff ] = ⊥
... | true | [ y≤x≡tt ] = I y x {≤ᵇ⇒≤ {!!}}

我有一个证人，(y ≤ᵇ x) ≡ true但我不知道如何使用它来结合它，≤ᵇ⇒≤以产生证人y ≤ x

agda

1 个回答

  1. Best Answer

    改用_≤?_：

    open import Relation.Nullary.Decidable.Core

_⊓𝕀_ : 𝕀 → 𝕀 → 𝕀
-∞ x ⊓𝕀 (y +∞) with y ≤? x
... | yes y≤x = I y x {y≤x}
... | no _ = ⊥

    要从字面上回答您的问题，您可以使用T-≡：≤ᵇ⇒≤ (Equivalence.from T-≡ y≤x≡tt)。

    • 3

相关问题