package coq-recursive-definition

  1. Overview
  2. No Docs
ML-like recursive definitions

Install

Dune Dependency

github.com Edit opam file Versions (2)

Authors

  1. A
    Antonia Balaa
  2. Y
    Yves Bertot

Maintainers

  1. H
    Hugo.Herbelin@inria.fr

Sources

v8.6.0.tar.gz
md5=d4df2f356bf846f882d8b2dadf38c3a9

Description

This module provides a facility to define recursive functions in an ML-like style, giving a fixpoint equation, a variant and a well-founded relation. A pure function is then generated, together with a theorem giving the fixpoint equation. THIS IS MAINLY A TEST CONTRIB, BEFORE INTEGRATION IN COQ.

Tags

keyword: recursive functions keyword: well-foundedness category: Miscellaneous/Coq Extensions date: 2002

Published: 20 Nov 2018

Dependencies (2)

  1. coq >= "8.6" & < "8.7~"
  2. ocaml

Dev Dependencies

None

Used by

None

Conflicts

None