package coq-antivalence

  1. Overview
  2. No Docs
A Coq plugin to generate type-inequality axioms for inductive definitions

Install

Dune Dependency

github.com Edit opam file Versions (2)

Authors

  1. I
    Isaac van Bakel

Maintainers

  1. I
    ivb@vanbakel.io

Sources

1.0.1.tar.gz
sha256=faa00b1dc21afef199f975815f6f69e0fc122ce249b5179bc946529c450d5608

Description

Antivalence generates universally-quantified type inequality axioms, letting you treat the set of inductive definitions in your program as a closed inductive definition itself.

Tags

category:Miscellaneous/Coq Extensions logpath:Antivalence date:2020-08-24

Published: 24 Aug 2020

Dependencies (1)

  1. coq >= "8.11" & < "8.12~"

Dev Dependencies

None

Used by

None

Conflicts

None