mirror of
https://github.com/larstvei/dot-emacs.git
synced 2024-11-26 07:28:31 +00:00
use-package proof-general
This commit is contained in:
parent
0f7a29d0fa
commit
82f363e3e0
17
init.org
17
init.org
@ -207,8 +207,7 @@
|
|||||||
|
|
||||||
(let* ((package--builtins nil)
|
(let* ((package--builtins nil)
|
||||||
(packages
|
(packages
|
||||||
'(proof-general ; A generic Emacs interface for proof assistants
|
'(racket-mode ; Major mode for Racket language
|
||||||
racket-mode ; Major mode for Racket language
|
|
||||||
rustic ; Rust development environment
|
rustic ; Rust development environment
|
||||||
slime ; Superior Lisp Interaction Mode for Emacs
|
slime ; Superior Lisp Interaction Mode for Emacs
|
||||||
try ; Try out Emacs packages
|
try ; Try out Emacs packages
|
||||||
@ -1657,10 +1656,24 @@
|
|||||||
|
|
||||||
** Coq
|
** Coq
|
||||||
|
|
||||||
|
[[https://proofgeneral.github.io/][Proof General]] is really great for working with proof assistants. I have only
|
||||||
|
tried it with Coq.
|
||||||
|
|
||||||
|
#+begin_src emacs-lisp
|
||||||
|
|
||||||
|
;; A generic Emacs interface for proof assistants
|
||||||
|
(use-package proof-general
|
||||||
|
:defer t)
|
||||||
|
|
||||||
|
#+end_src
|
||||||
|
|
||||||
|
For completions, I use [[https://github.com/cpitclaudel/company-coq][company-coq]].
|
||||||
|
|
||||||
#+begin_src emacs-lisp
|
#+begin_src emacs-lisp
|
||||||
|
|
||||||
;; A collection of extensions PG's Coq mode
|
;; A collection of extensions PG's Coq mode
|
||||||
(use-package company-coq
|
(use-package company-coq
|
||||||
|
:defer t
|
||||||
:hook (coq-mode . company-coq-mode))
|
:hook (coq-mode . company-coq-mode))
|
||||||
|
|
||||||
#+end_src
|
#+end_src
|
||||||
|
Loading…
Reference in New Issue
Block a user