syntax - Agda. Pattern matching on characters
问题描述
I've tried to implement my version of "sprintf" function (which constructs a string from a format string a number of arguments of different types), but failed. Same technique worked in Idris.
module Printf where
open import Agda.Builtin.List
open import Agda.Builtin.Char
open import Agda.Builtin.String
open import Agda.Builtin.Float
open import Agda.Builtin.Int
data Format : Set where
TChar : Char → Format → Format
TString : Format → Format
TFloat : Format → Format
TInt : Format → Format
TEnd : Format
parseFormat : List Char → Format
parseFormat ('%' :: 's' :: rest) = TString (parseFormat rest)
parseFormat ('%' :: 'f' :: rest) = TFloat (parseFormat rest)
parseFormat ('%' :: 'd' :: rest) = TInt (parseFormat rest)
parseFormat ('%' :: '%' :: rest) = TChar '%' (parseFormat rest)
parseFormat (x :: rest) = TChar x (parseFormat rest)
parseFormat [] = TEnd
But I get this error by the compiler:
Could not parse the left-hand side parseFormat ('%' :: 's' :: rest)
Operators used in the grammar:
None
when scope checking the left-hand side
parseFormat ('%' :: 's' :: rest) in the definition of parseFormat
Is it possible to pattern-match on characters like '1', 't', 'O' in Agda?
解决方案
推荐阅读
- azure-blob-storage - Cannot use azcopy from one blob to another with SAS
- pyspark - 将 jupyter sparkmagic 内核连接到 kerberized livy 服务器的问题
- python-3.x - 此代码未给出新排序列表的值。有人可以告诉我这段代码中的错误吗?
- python - Find N largest elements in a list with a minimum distance
- python - 如何使用 pandas 合并绘图表上的标题?
- hyperledger-fabric - 如何解决此错误 Blockchain_chaincode
- c# - 是否可以在父目录中构建文件?
- javascript - 使用nestjs将hbs渲染保存到变量中
- reactjs - 使用 Typescript 映射对象数组
- javascript - 分配给 axios 响应数据的变量会破坏应用程序