Idris2 with rational package template

default.nix

{ nixpkgs ? import <nixpkgs> {} }:
let
  inherit (nixpkgs)
  fetchFromGitea
  mkShell
  idris2Packages;

  inherit (idris2Packages) buildIdris idris2 idris2Lsp;

  rationalPkg = buildIdris {
    src = fetchFromGitea {
      domain = "git.envs.net";
      owner = "iacore";
      repo = "idris2-rational";
      rev = "main";
      hash = "sha256-2QnDhaRsJahKszGD3rMTnOv45TBbBt8pubnmLY6sSbw=";
    };
    ipkgName = "rational";
    idrisLibraries = [];
  };

  myPkg = buildIdris {
    src = ./.;
    ipkgName = "my-pkg";
    idrisLibraries = [ rationalPkg ];
  };
in
rec {
  package = myPkg.library {};
  # alternatively, if building an executable:
  # package = myPkg.executable;

  shell = mkShell {
    packages = [
      idris2
      idris2Lsp
    ];

    inputsFrom = [
      package
    ];
  };
}

my-pkg.ipkg

package mypkg

depends = rational

modules = MyPackage

MyPackage.idr

module MyPackage

import Data.Rational

export
doThing : () -> Rational
doThing = ?hole