Block or report user


@coq @HoTT @math-classes

Popular repositories

  1. Coq-Equations

    A plugin for Coq to add dependent pattern-matching.

    OCaml 27 5

  2. Constructors

    Example Coq plugin

    OCaml 12 3

  3. Forcing

    Forcing layer on top of Coq

    Coq 6 1

  4. coq

    Forked from 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

  5. Coq--RTL

    A formalization of λRTL in Coq

    Verilog 2

  6. math-classes

    Forked from robbertkrebbers/math-classes

    Verilog 2

413 contributions in the last year

Mar Apr May Jun Jul Aug Sep Oct Nov Dec Jan Feb Mon Wed Fri

Contribution activity First pull request First issue First repository Joined GitHub

February 2017

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

Univs: fix bug #5365, generation of u+k <= v constraints

The twist used to handle template polymorphic inductives making their conclusion always algebraic was a bit too strong, sometimes the universe cann…

Seeing something unexpected? Take a look at the GitHub profile guide.