coq-equations

Function definition plugin for Coq

Equations provides a notation for writing programs by dependent pattern-matching and (well-founded) recursion in Coq. It compiles everything down to eliminators for inductive types, equality and accessibility, providing a definitional extension to the Coq kernel.

Versions: 1.3-8.18
Website: https://mattam82.github.io/Coq-Equations/
Licenses: LGPL 2.1
Package source: gnu/packages/coq.scm
Builds: See build status
Issues: See known issues

Installation

Install the latest version of coq-equations as follows:

guix install coq-equations

Or install a particular version:

guix install coq-equations@1.3-8.18

You can also install packages in augmented, pure or containerized environments for development or simply to try them out without polluting your user profile. See the guix shell documentation for more information.

Badge code

You can use the following badge to inform users of coq-equations about the latest version available in Guix.

Example HTML:

<a href='https://packages.guix.gnu.org/packages/coq-equations'><img src='https://packages.guix.gnu.org/packages/coq-equations/badges/latest-version.svg' alt='Version in GNU Guix'></a>

Example Markdown:

[![Version in GNU Guix](https://packages.guix.gnu.org/packages/coq-equations/badges/latest-version.svg)](https://packages.guix.gnu.org/packages/coq-equations)

Example Org:

[[https://packages.guix.gnu.org/packages/coq-equations][https://packages.guix.gnu.org/packages/coq-equations/badges/latest-version.svg]]