Zongyuan Liu comments

Repositories
Issues
Comments

Results 5 comments of


                                            Zongyuan Liu

Document the pitfall of modifying `lean4-mode-hook` before Lean4-Mode has been loaded

I can confirm both the issue and the fix.

Recent MR to support rocq binary broke "hacks" that allow changing coq-prog-name

I encountered a similar issue after upgrading PG. I set `proof-prog-name` in my emacs config file, but the code quoted above always overwrites my config.

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

#8132 might fix it.

ispecialize terms of the form P ∗ Q -∗ R

I'm interested in implementing specialization patterns and improving `ispecialize`. Since @oliversoeser's `iapply` PR #80 already implements some of the specialization patterns and Proof mode terms, such effort should build on...

Selection Patterns

Hi, I'm working on it.