package coq-sflib

  1. Overview
  2. Homepage
A collection of useful Rocq lemmas and tactics

Install

Dune Dependency

github.com Edit opam file Versions (1)

Authors

  1. J
    Jeehoon Kang <jeehoon.kang@kaist.ac.kr>
  2. M
    Minki Cho <minki.cho@sf.snu.ac.kr>
  3. J
    Jaehyung Lee <jaehyung.lee@sf.snu.ac.kr>
  4. Y
    Yeji Han <yeji.han@sf.snu.ac.kr>
  5. G
    Gil Hur <gil.hur@sf.snu.ac.kr>

Maintainers

  1. Y
    yeji.han@sf.snu.ac.kr

Sources

2.1.0.tar.gz
sha512=cb8af729fd765fae1663a836ebf491251f99aab313372b4d11efbb7f0d4b9e3b087f3c42997a4648114e56a619a1c540a8f2893802f60e1c99664267f8752863

Description

This package provides useful Rocq lemmas and tactics for proof automation and rewriting.

Tags

date:2026-02-20 category:Computer Science/Programming Languages/Formal Definitions and Theory keyword:tactics keyword:lemmas keyword:proof automation logpath:sflib

Published: 20 Feb 2026

Dependencies (3)

  1. dune >= "3.8"
  2. rocq-stdlib
  3. coq-core >= "9.0"

Dev Dependencies (1)

  1. odoc with-doc

Used by

None

Conflicts

None

Rocq

Interactive Theorem Prover

Zulip GitHub Discourse Mastodon RSS
About
Changelog Releases Industrial Users Academic Users History Why Rocq? Roadmap
Ecosystem
Platform Packages Rocq Team Community Consortium Events Rocq Planet Jobs
Resources
Install Rocq Get Started Documentation Books Papers Logo
Policies
Governance Privacy Code of Conduct