equational-reasoning-induction: Proof assistant for Haskell using DataKinds & PolyKinds

[ bsd3, library, math ] [ Propose Tags ] [ Report a vulnerability ]

A simple convenient library to write equational / preorder proof as in Agda. This package depends on singletons and generates induction schemes.

Downloads

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Candidates

  • No Candidates
Versions [RSS] 0.6.0.0
Dependencies base (>=4 && <5), semigroups (>=0.18 && <0.19), singletons, template-haskell (>=2.11 && <2.16), th-extras (>=0.0 && <0.1) [details]
Tested with ghc ==8.0.2, ghc ==8.2.2, ghc ==8.4.1, ghc ==8.6.3
License BSD-3-Clause
Copyright (c) Hiromi ISHII 2013-2018
Author Hiromi ISHII
Maintainer konn.jinro_at_gmail.com
Category Math
Source repo head: git clone git://github.com/konn/equational-reasoning-induction.git
Uploaded by HiromiIshii at 2019-02-08T13:49:36Z
Distributions
Downloads 600 total (4 in the last 30 days)
Rating (no votes yet) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs available [build log]
Last success reported on 2019-02-08 [all 1 reports]