Block or report user

Report or block pi8027

Hide content and notifications from this user.

Contact Support about this user’s behavior.

Report abuse


@coins11 @itplanning @tcug

Pinned repositories

  1. lambda-calculus

    A Formalization of Typed and Untyped λ-Calculi in SSReflect-Coq and Agda2

    Coq 35 4

  2. typeinfer

    Type inference in OCaml

    TeX 33 2

  3. formalized-postscript

    PostScript programming in the Coq proof assistant

    Coq 7 1

54 contributions in the last year

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

Contribution activity

July 2018

Created a pull request in math-comp/math-comp that received 3 comments

Replace all the CoInductives with Variants

The MathComp library uses many CoInductive commands to build non-recursive type families without generating inductive principles. I think that it c…

+85 −85 3 comments

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