Zongyuan Liu

icon indicating a website link cs.au.dk/~zyliu

icon company @logsem icon location Aarhus icon location PhD student in formal verification

Results 2 issues of Zongyuan Liu

Couldn't enable `opam-switch-mode` in Coq projects

5 comment

### I confirm that... - [X] I have searched the [issue tracker](https://github.com/doomemacs/doomemacs/issues), [documentation](https://docs.doomemacs.org), [FAQ](https://docs.doomemacs.org/-/faq), [Discourse](https://discourse.doomemacs.org), and [Google](https://google.com), in case this issue has already been reported/resolved. - [X] I have read...

is:bug
needs-triage

Improving `ipose`

TODO: Needs clean up This PR improves `ipose` in the following ways: 1. Support posing arbitrary terms (e.g. global theorems), not just local hypotheses, via `elabTerm`. 2. Following Rocq, unified...