Kindelia/Kind2
1
1
Fork 0
mirror of https://github.com/Kindelia/Kind2.git synced 2024-09-11 07:15:45 +03:00
Code Issues Projects Releases Wiki Activity

Merge branch 'master' of https://github.com/uwu-tech/Kind

Browse Source
This commit is contained in:
rheidner 2021-10-20 14:38:51 -03:00
commit 6117e74228
2 changed files with 39 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
base/Nat/mul/equal_zero.kind Normal file
View File

@ -0,0 +1,16 @@
Nat.mul.equal_zero(
n: Nat, m: Nat
Hyp: Equal<Nat>(Nat.mul(n, m), 0)
): Or<Equal<Nat>(n, 0), Equal<Nat>(m, 0)>
case n with Hyp {
zero:
left(refl)
succ:
case m with Hyp {
zero:
right(refl)
succ:
let contra = Nat.succ_neq_zero!(Hyp)
Empty.absurd!(contra)
}!
}!

24
flake.nix
View File

@ -8,7 +8,7 @@
flake-utils.lib.eachDefaultSystem (system:
let
pkgs = nixpkgs.legacyPackages.${system};
version = "1.0.95";
version = "1.0.104";
in
{
packages.kind-scm =
@ -33,6 +33,28 @@
doCheck = false;
};
packages.kind-scm-deb =
pkgs.stdenv.mkDerivation {
pname = "kind-scm-deb";
version = version;
src = self;
buildInputs = [ pkgs.chez-racket pkgs.chez-exe pkgs.libuuid pkgs.dpkg ];
buildPhase = ''
cd bin/scm
make deb
'';
installPhase = ''
mkdir -p $out
cp bin/kind-scm_1.0.1-0_amd64.deb $out
'';
doCheck = false;
};
/*packages.kind-js =
pkgs.stdenv.mkDerivation {
pname = "kind-js";