first working config

README.md

@@ -1,2 +1,12 @@
 # agdaTemplate
+This is my agda project config template, use it if you want to.
+I will not provide documentation above the notes to myself, and it
+may or may not work at any given point in time.
+
+- [ ] get the emacs config contained to the project
+```  
+(require 'evil)
+(evil-mode 1)
+(load-theme 'dracula t)
+```
 

flake.nix

@@ -0,0 +1,51 @@
+{
+  description = "Description for the project";
+
+  inputs = {
+    flake-parts.url = "github:hercules-ci/flake-parts";
+    nixpkgs.url = "github:NixOS/nixpkgs/nixos-unstable";
+  };
+
+  outputs = inputs@{ flake-parts, ... }:
+    flake-parts.lib.mkFlake { inherit inputs; } {
+      imports = [
+        # To import a flake module
+        # 1. Add foo to inputs
+        # 2. Add foo as a parameter to the outputs function
+        # 3. Add here: foo.flakeModule
+      ];
+      systems = [ "x86_64-linux" "aarch64-linux" "aarch64-darwin" "x86_64-darwin" ];
+      perSystem = { config, self', inputs', pkgs, system, ... }: {
+        # Per-system attributes can be defined here. The self' and inputs'
+        # module parameters provide easy access to attributes of the same
+        # system.
+
+        # Equivalent to  inputs'.nixpkgs.legacyPackages.hello;
+        devShells.default = pkgs.mkShellNoCC {
+          inputsFrom = [];
+          packages =
+            let
+              emacsWithPackages = (pkgs.emacsPackagesFor pkgs.emacs-nox).emacsWithPackages;
+              myEmacs = emacsWithPackages (epkgs: with epkgs;
+                [
+                  agda2-mode
+                  evil
+                  dracula-theme
+                ]
+              );
+            in
+          with pkgs; [
+            # https://ryantm.github.io/nixpkgs/languages-frameworks/agda/
+            (agda.withPackages (p : [ p.standard-library ]))
+            myEmacs
+          ];
+        };
+      };
+      flake = {
+        # The usual flake attributes can be defined here, including system-
+        # agnostic ones like nixosModule and system-enumerating ones, although
+        # those are more easily expressed in perSystem.
+
+      };
+    };
+}

project.agda-lib

@@ -0,0 +1,3 @@
+name: project
+depend: standard-library
+include: src

src/hello-world-dep.agda

@@ -0,0 +1,9 @@
+module hello-world-dep where
+
+open import Data.Nat using (ℕ; zero; suc)
+
+data Vec (A : Set) : ℕ → Set where
+  [] : Vec A zero
+  _::_ : ∀ {n} (x : A) (xs : Vec A n) → Vec A (suc n)
+
+infixr 5 _::_