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

一元化不减量

agda

MaiaVictor · 技术社区 · 7 年前

当要求Agda正常化时 test 在以下程序中:

data Bool : Set where
  T : Bool
  F : Bool
{-# BUILTIN BOOL  Bool  #-}
{-# BUILTIN TRUE  T #-}
{-# BUILTIN FALSE F #-}

postulate String : Set
postulate primStringEquality : String â String â Bool
{-# BUILTIN STRING String #-}

test : Bool
test = primStringEquality "bar" "foo"

它回来了 primStringEquality "bar" "foo" 而不是 F . 为什么?

1 回复 | 直到 7 年前

András Kovács 7 年前

它是 primitive 为了平等而不是 postulate . 我们还要申报 BUILTIN STRING

postulate String : Set
{-# BUILTIN STRING String #-}

primitive primStringEquality : String â String â Bool

推荐文章

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。外国金融机构

8 年前

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

9 年前

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

9 年前

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

10 年前