diff --git a/README.md b/README.md index bf53851..121d023 100644 --- a/README.md +++ b/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) +``` diff --git a/flake.nix b/flake.nix new file mode 100644 index 0000000..4f821f0 --- /dev/null +++ b/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. + + }; + }; +} diff --git a/project.agda-lib b/project.agda-lib new file mode 100644 index 0000000..f6824ac --- /dev/null +++ b/project.agda-lib @@ -0,0 +1,3 @@ +name: project +depend: standard-library +include: src diff --git a/src/hello-world-dep.agda b/src/hello-world-dep.agda new file mode 100644 index 0000000..ff73a77 --- /dev/null +++ b/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 _::_