jwaldmann

As I'm planning to use this in an online system: could this be DoS-ed? Are there short proofs where checking would be expensive? But the proof language is rather explicit...

README.md says ``` .=. ``` but this should be ``` (by ) .=. ```

( https://wiki.haskell.org/Wadler%27s_Law ) Since cyp is about proving things about Haskell programs, I expect line "--" and block "{- .. -}" comments to work. These may be useful while working...

inconsistent spelling (capitalization): goal, Lemma

2

* in theory texts, lower case: axiom, goal. * in proof texts: upper case: Lemma, Proof, QED, IH * ... and lower case: def I find upper case very inconvenient...

for consistency with other named equations (axiom, lemma), goal syntax should: * have a colon * allow a name (?) So, not `goal non . not .=. id` but `goal...

Named induction hypotheses

5

I made this example https://gitlab.imn.htwk-leipzig.de/waldmann/cyp/tree/master/test-data/pos/bintree and I was surprised that I could write two IHs: ``` Case Branch l k r To show: (inorder . mirror) (Branch l k r)...

proof by induction on List xs - but the type of xs is List a

1

This uses an identifier `xs` ``` Proof by induction on List xs ``` but its type is *not* what's written there (the type argument is missing). This will super-confuse students...

theory syntax should allow type declarations

6

Not a bug. But I'd appreciate hints on how this feature could be implemented (relative to the current code base) most easily. I want to write ``` inorder :: Tree...

perhaps not that important, but when I tried to write a simple proof (without looking at examples), I fully expected that it's `by axiom `, by similarity to `by def...

Slow compilation

6

Just for reference, I noticed https://ghc.haskell.org/trac/ghc/ticket/15488 and I can confirm that compilation is slow. This is for accelerate-1.2.0.0 (current from hackage) with ghc-8.4.3 on GNU/Linux-amd64