Skip to content
View agrarpan's full-sized avatar
2 followers · 2 following

Achievements

Achievement: YOLO
BetaSend feedback

Achievements

Achievement: YOLO
BetaSend feedback
Block or Report

Block or report agrarpan

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.

Please don't include any personal information such as legal names or email addresses. Maximum 100 characters, markdown supported. This note will be visible to only you.
Report abuse

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

Report abuse

Pinned

  1. coq-synthesis coq-synthesis Public

    coq-synthesis is a Coq plugin for proof generation and next tactic prediction

    Coq 11 1

  2. proverbot9001-plugin proverbot9001-plugin Public

    Forked from UCSD-PL/proverbot9001

    For use with synthesis plugin

    Coq

  3. coq-plugin-lib coq-plugin-lib Public

    Forked from uwplse/coq-plugin-lib

    Library of useful utility functions for Coq plugins

    OCaml 2

  4. pumpkin-pi pumpkin-pi Public

    Forked from uwplse/pumpkin-pi

    An extension to PUMPKIN PATCH with support for proof repair across type equivalences.

    Coq 1

  5. fix-to-elim fix-to-elim Public

    Forked from uwplse/fix-to-elim

    Fixpoint to eliminator translation in Coq

    Coq 1