文件名称：schmitty:Agda与SMT-LIB2兼容求解器的绑定
文件大小：2.39MB
文件格式：ZIP
更新时间：2024-05-27 05:24:27
agda smt-solver Agda
施密特解算器 {-# OPTIONS --allow-exec #-} open import Data.Integer open import Data.List open import Data.Product open import Relation.Binary.PropositionalEquality open import SMT.Theories.Ints as Ints open import SMT.Backend.Z3 Ints.reflectable 如果您想解决一些问题，那您很幸运！ Schmitty是一个Agda库，可为您提供SMT求解器的绑定！ 我知道，很酷吧！ verycool : ∀ (x y : ℤ) → x ≤ y → y ≤ x → x ≡ y verycool = solveZ3 因此，基本上，Schmitty为您提供的是在Agda中很好地嵌