The Wayback Machine - https://web.archive.org/web/20201213170147/https://github.com/mattam82
Skip to content
Avatar
  • Block or report user

    Block or report mattam82

    Report abuse

    Contact GitHub support about this user’s behavior. Learn more about reporting abuse.

    Report abuse
119 followers · 0 following · 9

Highlights

  • Arctic Code Vault Contributor

Organizations

@coq @HoTT @math-classes

Pinned

  1. coq/coq

    Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive develo…

    OCaml 3.1k 489

  2. MetaCoq/metacoq

    Metaprogramming in Coq

    Coq 187 45

  3. HoTT/HoTT

    Homotopy type theory

    Coq 928 153

  4. Coq-Equations

    A function definition package for Coq

    Coq 153 33

  5. coq/opam-coq-archive

    Archive for all Coq related OPAM packages organized in various repositories

    JavaScript 56 100

  6. unicoq/unicoq

    An enhanced unification algorithm for Coq

    OCaml 32 12

768 contributions in the last year

Dec Jan Feb Mar Apr May Jun Jul Aug Sep Oct Nov Dec Mon Wed Fri
Learn how we count contributions.
Less
More
Activity overview
Contributed to MetaCoq/metacoq, mattam82/Coq-Equations, coq/coq and 5 other repositories

Contribution activity

December 2020

Created 68 commits in 3 repositories

Created a pull request in coq/coq that received 18 comments

[kernel]Use ~l2r:true to restore previous order of unfolding

When typing predicates of cases. Apparently Kami is sensitive to that. Kind: performance Fixes / closes: comment in #13501 Added / updated test-s…

+5 −2 • 18 comments
Opened 5 other pull requests in 2 repositories
Reviewed 2 pull requests in 1 repository

Created an issue in coq/coq that received 4 comments

hnf on PrimFloat.of_int63 raises an anomaly

Description of the problem From Coq Require Import PrimFloat. Definition f := of_int63 1. Eval hnf in f. raises Anomaly "Uncaught exception Envir…

4 comments
You can’t perform that action at this time.