-
Notifications
You must be signed in to change notification settings - Fork 34
Issues: cpitclaudel/alectryon
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Author
Label
Projects
Milestones
Assignee
Sort
Issues list
Porting Alectryon to coqc or coq-lsp before coq-serapi is unmaintained
#97
opened Jul 22, 2024 by
tchajed
Alectryon displays local definitions (with set, pose) as declarations
#94
opened Nov 20, 2023 by
Casteran
Some links of Lean recipes in README are broken due to inconsistent naming
#82
opened Aug 1, 2022 by
utensil
Feature wish: show types of top-level identifiers in definitions (on mouse hover)
#74
opened Nov 30, 2021 by
anton-trunov
alectryon.minimal
and a no-coq-serapi
use-case
kind: feature
status: implemented
status: pending
#60
opened Aug 16, 2021 by
jhaag
Printing inductive types as 2D inference rules?
status: pending
#53
opened Jul 16, 2021 by
anton-trunov
Syntax error: illegal begin of vernac. -- with indented comments
status: help wanted
#48
opened Jul 1, 2021 by
start974
Previous Next
ProTip!
Follow long discussions with comments:>50.