Qiyuan Zhao
Results
2
issues of
Qiyuan Zhao
Tried implementing a rudimentary message panel in the fashion of that in CoqIDE. Also including some modifications on the displaying style (see `html_views/src/goals/proof-view.css`). **Screenshots**: **Features**: - Output is highlighted (rendered...
Hi! I recently started experimenting with `lean-auto`, primarily to explore its support for SMT solvers. However, I frequently encounter errors ending with `Higher order input?`, which are not always very...