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

Agda:函数分析错误

agda parsing

mko · 技术社区 · 7 年前

谢谢你

data Shish (a : Set) : Set where
  Bottom : a â Shish a
  Onion : Shish a â Shish a
  Lamb : Shish a â Shish a
  Tomato : Shish a â Shish a

data Rod : Set where
  Dagger : Rod
  Fork : Rod
  Sword : Rod

data Plate : Set where
  Gold-plate : Plate
  Silver-plate : Plate
  Brass-plate : Plate

what_bottom : Shish (a : Set) â Bool
what_bottom (Bottom x) â x
what_bottom (Onion x) â what_bottom x
what_bottom (Lamb x) â what_bottom x
what_bottom (Tomato x) â what_bottom x



/Volumes/Little/mko_io/cat/tmp/mler.agda:54,24-24
        /Volumes/Little/mko_io/cat/tmp/mler.agda:54,24: Parse error
        :<ERROR>
         Set) â Bool
        what_bottom (Bott...

2 回复 | 直到 7 年前

white_wolf 7 年前

数据类型定义定义正确,但这不是在Agda中定义函数的方式。一个好的开始教程是 Dependent types at work

id : {A : Set} â A â A
id a = a

此外,依赖类型必须在like之前声明,所以要么隐式声明,要么显式声明。

what_bottom : {A : Set} â Shish A â ...

最后,不能用返回类型定义该函数 Bool a 不过。

Cactus 7 年前

作为附加的语法点,在Agda中,下划线是mixfix参数的占位符: what_bottom what 和 bottom . 所以你最终会得到一个函数 what (Onion $ Lamb $ Bottom) bottom 这可能不是你想要的。就叫它吧 whatBottom 或 whatâ¿bottom 如果你觉得多余。

推荐文章

David542 · 任何语言都允许函数名中有空格吗?

1 年前

Abbey A. · 从中的文本字符串中有条件地解析数字,并将其分配给R中的新列

1 年前

David542 · 为什么词法分析器通常将var定义为不能以数字开头?

1 年前

thenightmarechild92 · 使用正则表达式拆分具有唯一标题的子节

1 年前

Andy · 将LENGTH OF移动到COMP字段解析失败

2 年前

Chris Geo · 如何找到LR0项目的FOLLOW集合?

2 年前

Anton · 不能将运算符[]与数组的字符串参数一起使用(解析json)

2 年前

user25485370 · 如何在带分隔符的C++中解析字符串?[关闭]

2 年前

Yash Singhal · 在reactjs中解析Pdf中的文本

2 年前

i33SoDA · 如何将逗号分隔的数字字符串解析为int数组?

2 年前