【发布时间】：2017-07-23 02:39:44
【问题描述】：
前面有' 字符的名称是Type 类型：
Idris> 'foo
'foo : Type
这是什么意思？'foo 类型的值的示例是什么？
【问题讨论】：
标签： types syntax idris single-quotes
【发布时间】：2017-07-23 02:39:44
【问题描述】：
字符串值前面的前导单引号将该字符串转换为类型。它是prelude/Builtins.idr中定义的内置语法扩展
||| For 'symbol syntax. 'foo becomes Symbol_ "foo"
data Symbol_ : String -> Type where
如果我理解正确，符号没有值，而仅存在于类型级别。
idris 文档中记录了符号的一个用例：http://docs.idris-lang.org/en/latest/effects/state.html?highlight=symbol，其中符号用于标记具有其他相同类型签名的状态。
【讨论】：