Skip to content
Block or Report

Block or report SkySkimmer

Block user

Prevent this user from interacting with your repositories and sending you notifications. Learn more about blocking users.

You must be logged in to block users.

Add an optional note:
Report abuse

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

Report abuse

Popular repositories

  1. HoTT proofs using experimental induction-induction (mostly about real numbers) (used to contain the HoTT.Classes proofs)

    Coq 13 4

  2. HoTT-algebra Public archive

    Coq formalisation of algebra in Homotopy Type Theory

    Coq 6 1

  3. ZF Public

    Playing around with axiomatic set theory in Coq

    Coq 3 1

  4. dedukti Public

    A universal proof checker

    OCaml 2 1

  5. .emacs.d Public

    Emacs configuration

    Emacs Lisp 2

1,513 contributions in the last year

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

Contribution activity

September 2022

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

configure: remove coqide switch

It was basically a noop since the move to dune.

+24 −139 19 comments
Reviewed 36 pull requests in 2 repositories
coq/coq 25 pull requests
coq/ceps 1 pull request

Created an issue in coq/coq that received 5 comments

Error reporting when building stdlib has too short paths

put some error in a stdlib file, eg theories/Init/Logic.v dune build the error will be reported as File "./Logic.v", line XXX, characters XXX: bu…

Opened 4 other issues in 4 repositories
mit-plv/fiat-crypto 1 open
coq/coq 1 open
refined-github/refined-github 1 open
MetaCoq/metacoq 1 open

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