文件名称：coq-ceres:Coq库，用于序列化为S表达式
文件大小：37KB
文件格式：ZIP
更新时间：2024-06-08 19:05:57
serialization coq pretty-print debug Coq
塞雷斯 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类型：
【文件预览】：
coq-ceres-master
----coq-ceres.opam(542B)
----theories()
--------CeresDeserialize.v(13KB)
--------CeresUtils.v(840B)
--------Ceres.v(167B)
--------CeresSerialize.v(2KB)
--------CeresParserInternal.v(6KB)
--------dune(112B)
--------CeresParserRoundtrip.v(6KB)
--------CeresParser.v(776B)
--------CeresParserRoundtripProof.v(22KB)
--------CeresString.v(10KB)
--------CeresFormat.v(1KB)
--------CeresS.v(7KB)
--------CeresRoundtrip.v(10KB)
--------CeresParserUtils.v(1KB)
----.circleci()
--------config.yml(1KB)
----dune-project(50B)
----_CoqProject.dune(33B)
----LICENSE(1KB)
----test()
--------Test.v(3KB)
----README.md(7KB)
----Makefile(968B)
----tutorial()
--------Tutorial.v(7KB)
----.gitignore(305B)
----CHANGELOG.md(837B)
----_CoqProject.classic(353B)