search

elexunix / qock

This project is currently an implementation of a proof-checker. But it is planned to be extended; for example, to support algorithm extraction from intuitionistic proofs, which is considered to be an interesting feature.
0 stars 0 forks source link

Too verbose syntax #7

Open MikailBag opened 3 years ago

MikailBag commented 3 years ago

As you can see, currently advanced C++ template features are used. It makes a proof difficult to read.

Instead proofs should be written on DSL and then transpiled to C++ templates (either with a special compiler, or with a help of C++ defines).