Releases: snu-sf/paco
Releases · snu-sf/paco
Paco v4.0.0
- Support "paco" and "gpaco", and remove "gcpn".
- Support the following tactics for "gpaco".
ginit, gfinal, gunfold, gunfoldbot, gbase, gstep, gupaco, gclo, grclo, guclo, glecpn, gcofix
Paco v3.0.0
- Support "gcpn", which supports more general incremental principles.
- Add the following tactics:
gbase, gstep, gclo, gcpn, gcofix, gunfold, ginit, gfinal.
Paco v2.1.0
- Simplify the upto technique using "companion" following the following paper:
- Damien Pous, Coinduction All the Way Up, LICS 2016.
- Add tactics for upto reasoning:
uinit
,uunfold
,ubase
,ustep
,uclo
,ucofix
,ufinal
,ucompat
,gcpn_fold
.
Paco v2.0.3
- add the lemmas
[u]paco{n}_mon_bot
. - add the lemmas
rclo{n}_mon_gen
.
Paco v2.0.2
- improve
pclearbot
to work under binders. - export
Program.Basics
to support the notation forcompose
.
Paco v2.0.1
- improve the
pupto
tactic to just take the lemma name without arguments to the lemma. - add the lemmas
[u]paco{n}_mon_gen
.
Paco v2.0.0
- Support upto techniques.
- Remove the support of mutual coinduction but show how to do mutual coinduction using a single coinduction in the tutorial.
- Define paco using the negative form of CoInduction with primitive projections.
Makefile cleanup
fix Makefile (#4) * Update Makefile * make clean depends on Makefile.coq
Paco version 1.2.7
Initial release in GitHub