Pinned Repositories
baseconv
Base Conversion of Integers (from base 10 or 16 to Coq usual datatypes)
coq-debian-mingw32
coq-minicalc
Toy demo of lexing/parsing in Coq
coq-wip
Some Work-In-Progress stuff about Coq
cumul
explicit cumulativity
extraction-compute
A Coq plugin for computing Coq terms through extraction
hofstadter_g
Coq proofs about Hofstadter's function G
intellij-idea-dpkg
Makefile to create .deb files for Intellij IDEA
sketch-downloader
Download sketch.sh pages as markdown and {ocaml,reason} files
letouzey's Repositories
letouzey/coq-minicalc
Toy demo of lexing/parsing in Coq
letouzey/hofstadter_g
Coq proofs about Hofstadter's function G
letouzey/coq-wip
Some Work-In-Progress stuff about Coq
letouzey/sketch-downloader
Download sketch.sh pages as markdown and {ocaml,reason} files
letouzey/extraction-compute
A Coq plugin for computing Coq terms through extraction
letouzey/baseconv
Base Conversion of Integers (from base 10 or 16 to Coq usual datatypes)
letouzey/coq-debian-mingw32
letouzey/cumul
explicit cumulativity
letouzey/intellij-idea-dpkg
Makefile to create .deb files for Intellij IDEA
letouzey/numeral-notation
Custom parsing/printing for Coq numeral inductive types