以下阿格達代碼：
module test where
open import Data.Float
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_)
open Eq.≡-Reasoning using (begin_; _≡??_; step-≡; _?)
postulate
distrib : {m a b : Float} → m * (a b) ≡ (m * a) (m * b)
dbg : (m a b : Float) → m * (a b) ≡ (m * a) (m * b)
dbg m a b =
begin
m * (a b)
≡? distrib ? -- (Line "22")
(m * a) (m * b)
?
產量：
_m_18 : Float [ at /Users/dbanas/Documents/Agda/agda_misc/test.agda:22,6-13 ]
_a_19 : Float [ at /Users/dbanas/Documents/Agda/agda_misc/test.agda:22,6-13 ]
_b_20 : Float [ at /Users/dbanas/Documents/Agda/agda_misc/test.agda:22,6-13 ]
———— Errors ————————————————————————————————————————————————
Failed to solve the following constraints:
(_m_18 * _a_19) (_m_18 * _b_20) = (m * a) (m * b) : Float
_m_18 * (_a_19 _b_20) = m * (a b) : Float
在我輸入之后C-c C-l。
（注意： “22,6-13”表示第二次出現單詞“distrib”。）
我不明白為什么不能滿足約束條件。它們似乎很容易解決：
_m_18 = m
_a_19 = a
_b_20 = b
uj5u.com熱心網友回復：
雖然這些解決方案是正確的，但它們并非不可避免，因為乘法和加法不是單射的。在這種情況下，您可以只m在第 22 行填寫，即distrib {m = m}。
轉載請註明出處，本文鏈接：https://www.uj5u.com/net/536814.html
標籤：阿格达类型约束等式推理
上一篇：終止檢查失敗