agda - 关于如何使用 Agda 标准库幺半群求解器的示例

我正在开发一个带有很多无聊列表串联等式的代码，所以我想使用幺半群求解器。我知道模块 Algebra.Monoid-solver 实现了幺半群求解器，但我没有找到任何关于如何使用它的例子。

有人可以提供一个使用 stdlib monoid 求解器的快速示例吗？

最好的，

最佳答案

这是一个快速示例:

open import Relation.Binary.PropositionalEquality
open import Data.List
open import Data.List.Properties
open List-solver renaming (nil to :[]; _⊕_ to _:++_; _⊜_ to _:≡_)

assoc : {A : Set} (xs ys zs : List A) -> xs ++ (ys ++ zs) ≡ (xs ++ ys) ++ zs
assoc = solve 3 (λ xs ys zs -> xs :++ (ys :++ zs) :≡ (xs :++ ys) :++ zs) refl

Agda 可以部分推断类型签名:

assoc : {A : Set} (xs ys zs : List A) -> _
assoc = solve 3 (λ xs ys zs -> xs :++ (ys :++ zs) :≡ (xs :++ ys) :++ zs) refl

环形求解器也至少有两个前端: 1 和 2 ，你可以用类似的方式为幺半群求解器编写一个前端。

您是否考虑过使用具有定义关联性的差异列表？

也检查 this 线程。

关于agda - 关于如何使用 Agda 标准库幺半群求解器的示例，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/29216463/