orthologic-coqversion
A plugin to add orthologic-based tactics to Coq
Orthologic-based reasoning is super great. This plugin proposes a verified and optimized implementation of orthologic proof search, with memoization and pointer equality. It also provides an ocaml-based tactic that computes orthologic normal form, and a boolean tautology solver based on it.
| Tags | category:Miscellaneous/Coq Extensions keyword:orthologic logpath:OLCoq |
|---|---|
| Authors | Simon Guilloud and Clément Pit-Claudel |
| License | CC-BY-4.0 |
| Published | |
| Homepage | https://github.com/SimonGuilloud/orthologic-coq |
| Issue Tracker | https://github.com/SimonGuilloud/orthologic-coq/issues |
| Maintainer | Simon Guilloud |
| Available | arch != "arm32" & arch != "x86_32" |
| Dependencies | |
| Source [http] | https://github.com/SimonGuilloud/orthologic-coq/releases/download/v0.9.1/orthologic-coq-0.9.1.tbz sha256=60a9eeb27b6ad0a6fadb4127f5a7fdc194133dc55fa627e5eaedbee58a58651e sha512=bab767857cecbb1529e599785f2485e62171a55b7ec34483976a9a15e8223167c52a2977f88752e64f17fd1b4e6fde682b608bd046b2a7867da2eca10844cf57 |
| Edit | https://github.com/ocaml/opam-repository/tree/master/packages/orthologic-coq/orthologic-coq.0.9.1/opam |
No package is dependent
