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.0.tar.gz
sha256=a367cf9cd74b5fc644a23a802e695646ff688869363812295472f9baba60021f

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-05-06

Published: 06 May 2020

Dependencies (1)

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

Dev Dependencies

None

Used by

None

Conflicts

None