(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+)))