A proof of the problem TPP2011, called TPPmark
Switch branches/tags
Nothing to show
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
.gitignore
Half.agda
MinMaxLe.agda
README
State.agda

README

README
======

A proof of the TPPmark problem in Agda2, which is a translation in Coq.
The original proof in Coq is written by Jacques Garrigue.

http://staff.aist.go.jp/reynald.affeldt/tpp2011/ucd.html
http://staff.aist.go.jp/reynald.affeldt/tpp2011/garrigue_candy.v