No description, website, or topics provided.
Branch: master
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
LICENSE Add license Aug 30, 2017
Makefile Update Makefile to remove Ssreflect Coq 8.6 warnings Sep 5, 2017
README.md
_CoqProject Initial commit Jan 6, 2017
christodoulou.v
congestion.v
dist.v Finish proof that new CE -> CCE Dec 5, 2017
dyadic.v Cleanup Jan 6, 2017
dynamics.v Initial commit Jan 6, 2017
extrema.v Initial commit Jan 6, 2017
games.v Finish proof that new CE -> CCE Dec 5, 2017
numerics.v Update to Coq 8.6, Ssreflect 1.6.1 Aug 30, 2017
potential.v Change best_response to better_response Dec 19, 2017
routing.v Update potential class hierarchy slightly Jan 18, 2017
smooth.v Update defns. POA, POS to use Aug 14, 2017

README.md

A Library for Algorithmic Game Theory in Ssreflect/Coq

PREREQUISITES

  • Coq 8.6
  • Ssreflect 1.6.1

Alternatively, in OPAM, make sure you've installed the following packages:

coq                            8.6  Formal proof management system.
coq-mathcomp-algebra         1.6.1  Mathematical Components Library on Algebra
coq-mathcomp-fingroup        1.6.1  Mathematical Components Library on finite groups
coq-mathcomp-ssreflect       1.6.1  Small Scale Reflection

BUILD

Just type

make

in the top-level project directory.