hierarchy-builder

{
  "aliases": [],
  "alternatives": [],
  "build_dependencies": [],
  "categories": [],
  "caveats": null,
  "conflicts_with": [],
  "dependencies": [
    "rocq",
    "rocq-elpi"
  ],
  "deprecated": 0,
  "deprecation_reason": null,
  "desc": "High level commands to declare a hierarchy based on packed classes",
  "disable_reason": null,
  "disabled": 0,
  "enrichment_fetched_at": "2026-06-20T23:38:38+00:00",
  "first_seen": "2026-06-20T23:34:18+00:00",
  "full_name": "hierarchy-builder",
  "github_default_branch": "master",
  "github_last_commit_at": "2026-06-15T13:21:07Z",
  "github_readme_excerpt": "[![Actions Status](https://github.com/math-comp/hierarchy-builder/workflows/CI/badge.svg)](https://github.com/math-comp/hierarchy-builder/actions)\n[![project chat](https://img.shields.io/badge/zulip-join_chat-brightgreen.svg)](https://coq.zulipchat.com/#narrow/stream/237868-Hierarchy-Buidlder)\n\n\u003cimg align=\"right\" src=\"https://github.com/math-comp/hierarchy-builder/raw/master/etc/rocqy-hb.png\" alt=\"HB logo\" width=\"30%\" /\u003e\n\n### Hierarchy Builder\n\nHierarchy Builder (HB) provides high level commands to declare a hierarchy of algebraic structure\n(or interfaces if you prefer the glossary of computer science) for the Coq system.\n\nGiven a structure one can develop its theory, and that theory becomes automatically applicable to\nall the examples of the structure. One can also declare alternative interfaces, for convenience\nor backward compatibility, and provide glue code linking these interfaces to the structures part of\nthe hierarchy.\n\nHB commands compile down to Coq modules, sections, records, coercions, canonical structure instances\nand notations following the *packed classes* discipline which is at the core of the [Mathematical\nComponents](https://github.com/math-comp/math-comp) library. All that complexity is hidden behind\na few concepts and a few declarative Coq commands.\n\n## Example\n\n```coq\nFrom HB Require Import structures.\nFrom Coq Require Import ssreflect ZArith.\n\nHB.mixin Record IsAddComoid A := {\n  zero : A;\n  add : A -\u003e A -\u003e A;\n  addrA : forall x y z, add x (add y z) = add (add x y) z;\n  addrC : forall x y, add x y = add y x;\n  add0r : forall x, add zero x = x;\n}.\n\nHB.structure Definition AddComoid := { A of IsAddComoid A }.\n\nNotation \"0\" := zero.\nInfix \"+\" := add.\n\nCheck forall (M : AddComoid.type) (x : M), x + x = 0.\n```\n\nThis is all we need to do in order to declare the `AddComoid` structure\nand write statements in its signature.\n\nWe proceed by declaring how to obtain an Abelian group out of the\nadditive, commutative, monoid.\n\n```coq\nHB.mixin Record IsAbelianG",
  "github_repo": "math-comp/hierarchy-builder",
  "github_stars": 105,
  "github_topics": [
    "coq",
    "elpi",
    "mathcomp"
  ],
  "homepage": "https://github.com/math-comp/hierarchy-builder",
  "homepage_og_description": null,
  "homepage_og_image": null,
  "homepage_title": null,
  "installs_30d": 10,
  "installs_365d": 245,
  "installs_90d": 35,
  "keg_only": 0,
  "keg_only_reason": null,
  "last_seen": "2026-06-20T23:34:18+00:00",
  "license": "MIT",
  "llm_generated_at": null,
  "llm_model": null,
  "name": "hierarchy-builder",
  "oldnames": [],
  "one_liner": null,
  "optional_dependencies": [],
  "rank_30d": 8503,
  "rank_365d": 6849,
  "rank_90d": 8260,
  "raw_hash": "182f290e4b56d245",
  "recommended_dependencies": [],
  "revision": 4,
  "ruby_source_path": "Formula/h/hierarchy-builder.rb",
  "tap": "homebrew/core",
  "test_dependencies": [],
  "uses_from_macos": [],
  "version_head": null,
  "version_stable": "1.10.2",
  "versioned_formulae": [],
  "why_use_this": null
}