search

advancedresearch / poi

a pragmatic point-free theorem prover assistant
Apache License 2.0
136 stars 7 forks source link

Proof format #978

Open bvssvni opened 3 years ago

bvssvni commented 3 years ago

One idea is to have a human readable file format that can be checked automatically by Poi without search or standard library.

bvssvni commented 3 years ago

An idea is to use the logs from Poi-Reduce as the format. This will make it easy to use Poi-Reduce to produce proofs.

bvssvni commented 3 years ago

An idea is to use markdown, like the standard library.