blob: d0837b43e9a1bdd777d63b90eb22b3b860f6952e (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
|
(define-module (gnu packages rocq)
#:use-module (gnu packages autotools)
#:use-module (gnu packages base)
#:use-module (gnu packages coq)
#:use-module (gnu packages gawk)
#:use-module (guix build-system gnu)
#:use-module (guix download)
#:use-module (guix gexp)
#:use-module (guix git-download)
#:use-module (guix licenses)
#:use-module (guix packages))
(define-public lambda
(package
(name "lambda")
(version "0.0.1")
(source (origin
(method git-fetch)
(uri (git-reference
(url "git://git.rostovtsev.org/lambda")
(commit "v0.0.1")))
(sha256
(base32 ;; nix32
"0yk1shd3d6kz8pdbv11fg462kcvxvsw6lvmp7plqiiqicm4fbir4"))))
(build-system gnu-build-system)
(native-inputs (list coq
autoconf
automake ; alocal used here for some reason
which ; used in autoconf step
gawk ; used in autoconf step
))
(synopsis "Fundamental objects and results in the untyped lambda calculus.")
(description
(string-append
"A Rocq library for working with a weak call-by-value lambda calculus."
"Provides proofs of the Church-Rosser Properties and Uniform Confluence."))
(home-page "https://git.rostovtsev.org/lambda")
(license gpl3+)))
|
