coq-ceres:Coq库，用于序列化为S表达式

塞雷斯 Cérès是一个Coq库，用于序列化为S表达式。 S表达式 S表达式是结构化数据的统一表示。 例如，它们是Haskell中的Show和Rust中的Debug所使用的普通字符串的替代。 S表达式更适合程序使用，避免了自定义解析器并启用了灵活的格式化策略。 例子 这个S表达式... (example (message "I'm a teapot") (code 418)) ...对应于Coq中的此sexp 。 Definition example : sexp := [ Atom "example" ; [ Atom "message" ; Atom (Str "I'm a teapot") ] ; [ Atom "code" ; Atom 418%Z ] ]. 文献资料 是快速入门的好地方。 简化的概述 该库提供了带有两个构造函数的sexp类型：