gdp

Reason about invariants and preconditions with ghosts of departed proofs.

https://github.com/matt-noonan/gdp#readme

LTS Haskell 24.24:0.0.3.0
Stackage Nightly 2025-12-16:0.0.3.0
Latest on Hackage:0.0.3.0

See all snapshots gdp appears in

BSD-3-Clause licensed by Matt Noonan
Maintained by [email protected]
This version can be pinned in stack with:gdp-0.0.3.0@sha256:8633d032fb1e308418f327c9b7ce85c612a8b73f9056ea6a00e0f89d297ece0f,2076

Module documentation for 0.0.3.0

  • Data
    • Data.Arguments
    • Data.Refined
    • Data.The
  • GDP
  • Logic
    • Logic.Classes
    • Logic.Implicit
    • Logic.NegClasses
    • Logic.Proof
    • Logic.Propositional
  • Theory
    • Theory.Equality
    • Theory.Lists
    • Theory.Named
Depends on 3 packages(full list with versions):
base, gdp, lawful
Used by 1 package in nightly-2024-01-16(full list with versions):
gdp

gdp: Ghosts of Departed Proofs