Haitao Zhang

For frontend UI it could be just like this project though I don't know how easy it is to extract the framework from vscode. There are likely standalone project tree...

@edreamleo I hope you had a good sabbatical! Thanks for mentioning `leoflexx`. I just checked it out. While `flexx` seems quite magical the app itself, as you said, seems just...

@boltex Have you seen [the Code Server project](https://github.com/cdr/code-server)? They let you serve VSCode to the browser. I don't know how it works exactly. You may be able to figure that...

I dug a little deeper. Unification seems to behave differently based on the context: ``` Abella < Query ((F : i -> i) X) = (F X). No more solutions....

Meanwhile ```elpi``` seems to have both unification working: ``` goal> (F X) = (F X). Success: F = X0 X = X1 goal> pi F\ (F X) = (F X)....

Thanks for the explanation! I understand ```eq (F X) (F Y) :- eq X Y``` would not work in general as synthesizing the context F embodies much of the work...

@gnadathur97 Professor Nadathur, thanks for your responses! Suppose for a moment that I could convince Abella of the following: ``` Theorem eq_congr: forall F X Y, {eq X Y} ->...

I installed from opam and the version is 2.2.0. I experimented a little more in `vscode`. If I cut away the proofs from the examples in `tutorial.lp`, I get indications...

I have the same problem. What I found is that it only happens when the echoed string contains newlines ("\n"). Multiple echoes in a loop does not cause a problem.

After implementing a caching mechanism (through simple pure OCaml) all the modules listed in ```hol.ml``` can be loaded in slightly over 1s on an M1 MacBook Air. This is significantly...