# qed

**Repository Path**: mirrors_ndmitchell/qed

## Basic Information

- **Project Name**: qed
- **Description**: Experiments writing a prover
- **Primary Language**: Unknown
- **License**: BSD-3-Clause
- **Default Branch**: master
- **Homepage**: None
- **GVP Project**: No

## Statistics

- **Stars**: 0
- **Forks**: 0
- **Created**: 2020-09-25
- **Last Updated**: 2026-04-05

## Categories & Tags

**Categories**: Uncategorized

**Tags**: None

## README

# QED Prover [![Hackage version](https://img.shields.io/hackage/v/qed.svg?label=Hackage)](https://hackage.haskell.org/package/qed) [![Build Status](https://img.shields.io/travis/ndmitchell/qed.svg)](https://travis-ci.org/ndmitchell/qed)

Experiments writing a proof system, particularly designed to prove properties about Haskell code, such as the [HLint rewrite rules](https://github.com/ndmitchell/hlint/blob/master/data/Default.hs).

Tom Ellis described the approach as "coinduction on the execution".