package coq-libhyps

  1. Overview
  2. No Docs
Hypotheses manipulation library

Install

Dune Dependency

github.com Edit opam file Versions (11)

Authors

  1. P
    Pierre Courtieu

Maintainers

  1. P
    Pierre.Courtieu@lecnam.net

Sources

libhyps-1.0.1.tar.gz
md5=f15584ad68bc77a5bc06048abdd9aa0d

Description

This library defines a set of tactics to manipulate hypothesis indivually or by group. In particular it allows to apply a tactic on each hypothesis of a goal, or only new hypothesis after some tactic. Manipulations include: automatic renaming, decomposition, extracting premisses, but define your own manipulation on (groups of) hypothesis.

Tags

keyword:proof environment manipulation keyword:forward reasoning keyword:hypothesis naming

Published: 09 Jul 2020

Dependencies

None

Dev Dependencies (1)

  1. coq (>= "8.10" & < "8.14~") | (= "dev")

Used by (1)

  1. coq-hydra-battles >= "0.6"

Conflicts

None