Block or report user

Organizations

@CakeML @HOL-Theorem-Prover

Pinned repositories

  1. music

    original compositions

    LilyPond 2 1

  2. CakeML/cakeml

    CakeML: A Verified Implementation of ML

    Standard ML 254 19

  3. HOL-Theorem-Prover/HOL

    Canonical sources for HOL4 theorem-proving system. Branch master is where "mainline development" occurs.

    Standard ML 135 33

  4. machine-intelligence/Botworld.HOL

    An implementation of Botworld in Higher Order Logic

    Standard ML 6

  5. beeminder-clock

    Send your time spent clocked in to a Beeminder goal.

    Shell 3

  6. isabelle-opentheory

    Interface between Isabelle/HOL and OpenTheory

    Standard ML 1

1,266 contributions in the last year

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

Contribution activity First pull request First issue First repository Joined GitHub

March 2017

Created an issue in HOL-Theorem-Prover/HOL that received 35 comments

Add implicit NO_TAC to by

When one writes subgoal by tac the intended semantics is usually that tac solves the whole subgoal, but by allows tac to not fully solve the subgoa…

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