代码之家 › 专栏 › 技术社区 › user2667523

Agda标准库-为什么更多属性没有标记为抽象?

agda standard-library abstract

user2667523 · 技术社区 · 8 年前

在阿格达工作了几个月后,我才发现 abstract

用它来隐藏我的引理的工作 大大地 减少了键入检查我的程序所需的时间。然而,查看Agda标准库 摘要 很少使用。在我看来 Properties 文件(例如 Data.Nat.Properties )可能在 摘要 块,因为我想不出有什么用处来推理,例如,如何证明加法是可交换的。

这是一个抽象是一个新特性的例子,但它还没有进入标准库吗?或者标记校样有什么微妙之处或缺点吗 摘要 我失踪了?

1 回复 | 直到 8 年前

effectfully 8 年前

abstract 对于抽象事物,它会阻止计算,因此如果您在 摘要 subst 或 rewrite 同时仍保留正典性:

module _ where

open import Function
open import Relation.Binary.PropositionalEquality
open import Data.Nat.Base
open import Data.Fin hiding (_+_)

abstract
  +0 : â n -> n + 0 â¡ n
  +0  0      = refl
  +0 (suc n) = cong suc (+0 n)

zeroâ² : â n -> Fin (suc n + 0)
zeroâ² n = subst (Fin â suc) (sym (+0 n)) zero

fail : zeroâ² 2 â¡ zero
fail = refl

-- subst ((Î» {.x} â Fin) â suc) (sym (+0 2)) zero != zero of type Fin (suc 2 + 0)
-- when checking that the expression refl has type zeroâ² 2 â¡ zero

一、 e.一个 摘要 块具有与 postulate 块

如果您更换 摘要 具有 module _ where ,文件将键入check。

安德烈亚斯·阿贝尔 wrote :

我认为这个“抽象”的特征很少被理解。我们应该计划将其移除,给予5年的宽限期。如果没有其中一份是关于2020年之前的技术论文适当的语义及其与 meta,我们放弃它。

推荐文章

Kyle McKean · 带表达式非求值

7 年前

ice1000 · 当Agda/Idris无法做到时,Coq可以做什么?

7 年前

Cactus · 构建数据。列表全部来自另一个数据。列表全部的

7 年前

ice1000 · Agda的“重写”失败,出现一个提到变量“w”的错误

7 年前

luochen1990 · 如何在Idris/Agda/Coq中模式匹配多个值?

7 年前

M Farkas-Dyck · 如何消除冲突构造函数名称的歧义

7 年前

Adi Ostrov · Agda:无法执行IO-数据丢失。海外金融机构,IO。外国金融机构

7 年前

user2667523 · Agda标准库-为什么更多属性没有标记为抽象?

8 年前

Aadit M Shah · 如何使用Agda中N的归纳原理证明N的递归器的定义方程命题成立?

9 年前

m0davis · 从论点的顺序解释这种奇怪的影响(如果可能的话,提供一个解决方法)

9 年前