search

Lysxia / coq-ceres

Coq library for serialization to S-expressions
MIT License
18 stars 1 forks source link

Deserializers #1

Closed Lysxia closed 5 years ago

liyishuai commented 5 years ago

Any updates on deserializing? I'm seeking to include it in DeepWeb.

Lysxia commented 5 years ago

Here we go https://github.com/Lysxia/coq-ceres/blob/6758510967ce6799e25bf0a7a71b485cf0721425/theories/Deserialize.v

liyishuai commented 5 years ago

https://github.com/Lysxia/coq-ceres/blob/49fa70b89cc4c236b338adef409432ee93a8f0e6/theories/Deserialize.v#L123-L133 Concrete input-output examples would make it more comprehensible.

liyishuai commented 5 years ago

For now I always need to handwrite both Serialize and Deserialize instances. Time for lenses?

Lysxia commented 5 years ago

Time for a plugin!