Block or report user

Organizations

@impega @coqtail @msp-strath

Pinned repositories

  1. generic-syntax

    A Scope-and-Type Safe Universe of Syntaxes with Binding, Their Semantics and Proofs

    Makefile 9 1

  2. type-scope-semantics

    A self-contained repository for the paper Type and Scope Preserving Semantics

    Agda 11 2

  3. typing-with-leftovers

    Self-contained repository for the eponymous paper

    Agda 10

  4. agdarsec

    Total Parser Combinators in Agda

    Agda 9 1

  5. agdARGS

    Dealing with Flags and Options

    Agda 7 2

  6. potpourri

    Where everyday research happens

    Agda 15 2

543 contributions in the last year

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

Contribution activity First pull request First issue First repository Joined GitHub

October 2017

Created a pull request in agda/agda-stdlib that received 2 comments

[ generalize ] Level-polymorphic covec

Noticed this was not level polymorphic whilst working on #174

Created an issue in agda/agda-stdlib that received 2 comments

Add proof irrelevance proofs for common relations

The shape of a proof _≤_ on is for instance completely determined by the two natural numbers involved. I am sure there are plenty of similar low …

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