feat(emacs): Basic Agda configuration
This commit is contained in:
@@ -1,51 +0,0 @@
|
|||||||
{ config, lib, pkgs, niri, ... }:
|
|
||||||
|
|
||||||
with lib;
|
|
||||||
|
|
||||||
let
|
|
||||||
cfg = config.sydnix.niri;
|
|
||||||
in {
|
|
||||||
options = {
|
|
||||||
sydnix.niri = {
|
|
||||||
enable = mkEnableOption "Niri";
|
|
||||||
};
|
|
||||||
};
|
|
||||||
|
|
||||||
imports = [
|
|
||||||
niri.nixosModules.niri
|
|
||||||
];
|
|
||||||
|
|
||||||
config = mkIf cfg.enable {
|
|
||||||
|
|
||||||
programs.niri = {
|
|
||||||
enable = true;
|
|
||||||
};
|
|
||||||
|
|
||||||
services.pipewire.enable = true;
|
|
||||||
|
|
||||||
# programs.niri.enable = true;
|
|
||||||
|
|
||||||
# hardware = {
|
|
||||||
# graphics = {
|
|
||||||
# enable = true;
|
|
||||||
# extraPackages = with pkgs; [
|
|
||||||
# intel-media-sdk
|
|
||||||
# mesa
|
|
||||||
# ];
|
|
||||||
# enable32Bit = true;
|
|
||||||
# };
|
|
||||||
# nvidia = {
|
|
||||||
# open = false;
|
|
||||||
# modesetting.enable = true;
|
|
||||||
# };
|
|
||||||
# };
|
|
||||||
|
|
||||||
# environment.systemPackages = with pkgs; [
|
|
||||||
# fuzzel
|
|
||||||
# ];
|
|
||||||
|
|
||||||
# services.xserver.videoDrivers = [ "qxl" "nvidia" ];
|
|
||||||
# services.qemuGuest.enable = true;
|
|
||||||
# services.spice-vdagentd.enable = true;
|
|
||||||
};
|
|
||||||
}
|
|
||||||
42
users/crumb/programs/emacs/modules/lang/syd-lang-agda.el
Normal file
42
users/crumb/programs/emacs/modules/lang/syd-lang-agda.el
Normal file
@@ -0,0 +1,42 @@
|
|||||||
|
;;; syd-lang-agda.el -*- lexical-binding: t; -*-
|
||||||
|
|
||||||
|
(with-eval-after-load 'agda2
|
||||||
|
(general-define-key
|
||||||
|
:keymaps 'agda2-mode-map
|
||||||
|
:states '(normal visual motion emacs insert)
|
||||||
|
:major-modes t
|
||||||
|
:prefix syd-localleader-key
|
||||||
|
:non-normal-prefix syd-alt-localleader-key
|
||||||
|
"?" #'agda2-show-goals
|
||||||
|
"." #'agda2-goal-and-context-and-inferred
|
||||||
|
"," #'agda2-goal-and-context
|
||||||
|
"=" #'agda2-show-constraints
|
||||||
|
"SPC" #'agda2-give
|
||||||
|
"a" #'agda2-mimer-maybe-all
|
||||||
|
"b" #'agda2-previous-goal
|
||||||
|
"c" #'agda2-make-case
|
||||||
|
"d" #'agda2-infer-type-maybe-toplevel
|
||||||
|
"e" #'agda2-show-context
|
||||||
|
"f" #'agda2-next-goal
|
||||||
|
"gG" #'agda2-go-back
|
||||||
|
"h" #'agda2-helper-function-type
|
||||||
|
"l" #'agda2-load
|
||||||
|
"n" #'agda2-compute-normalised-maybe-toplevel
|
||||||
|
"p" #'agda2-module-contents-maybe-toplevel
|
||||||
|
"r" #'agda2-refine
|
||||||
|
"s" #'agda2-solveAll
|
||||||
|
"t" #'agda2-goal-type
|
||||||
|
"w" #'agda2-why-in-scope-maybe-toplevel
|
||||||
|
"x c" #'agda2-compile
|
||||||
|
"x d" #'agda2-remove-annotations
|
||||||
|
"x h" #'agda2-display-implicit-arguments
|
||||||
|
"x q" #'agda2-quit
|
||||||
|
"x r" #'agda2-restart)
|
||||||
|
(general-def
|
||||||
|
:keymaps 'agda2-mode-map
|
||||||
|
:states '(motion normal)
|
||||||
|
"[ n" #'agda2-previous-goal
|
||||||
|
"] n" #'agda2-next-goal)
|
||||||
|
(setq agda2-fontset-name "JuliaMono"))
|
||||||
|
|
||||||
|
(provide 'syd-lang-agda)
|
||||||
@@ -1,6 +1,7 @@
|
|||||||
(add-to-list 'load-path
|
(add-to-list 'load-path
|
||||||
(file-name-concat user-emacs-directory "modules" "lang"))
|
(file-name-concat user-emacs-directory "modules" "lang"))
|
||||||
|
|
||||||
|
(require 'syd-lang-agda)
|
||||||
(require 'syd-lang-emacs-lisp)
|
(require 'syd-lang-emacs-lisp)
|
||||||
(require 'syd-lang-clojure)
|
(require 'syd-lang-clojure)
|
||||||
(require 'syd-lang-nix)
|
(require 'syd-lang-nix)
|
||||||
|
|||||||
Reference in New Issue
Block a user