Skip to content
View pi8027's full-sized avatar
174 followers · 13 following

Achievements

Achievement: Pair Extraordinairex2Achievement: Pull Sharkx3Achievement: Arctic Code Vault ContributorAchievement: Starstruck

Achievements

Achievement: Pair Extraordinairex2Achievement: Pull Sharkx3Achievement: Arctic Code Vault ContributorAchievement: Starstruck

Organizations

@math-comp

Block or report pi8027

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

  • math-comp Public

    Forked from math-comp/math-comp

    Mathematical Components

    Coq 2 Updated Nov 18, 2024

  • nixpkgs Public

    Forked from NixOS/nixpkgs

    Nix Packages collection & NixOS

    Nix MIT License Updated Nov 18, 2024

  • kaobook Public

    Forked from fmarotta/kaobook

    A LaTeX class for books, reports or theses based on https://github.com/kenohori/thesis and https://github.com/Tufte-LaTeX/tufte-latex.

    TeX 1 LaTeX Project Public License v1.3c Updated Nov 12, 2024

  • stablesort Public

    Stable sort algorithms and their stability proofs in Coq

    coq mergesort insertion-sort sorting-algorithms ssreflect mathcomp
    Coq 22 1 Updated Sep 11, 2024

  • pi8027 Public

    My profile README.md

    Updated Sep 6, 2024

  • opam-coq-archive Public

    Forked from coq/opam

    Archive for all Coq related OPAM packages organized in various repositories

    OCaml 1 GNU Lesser General Public License v2.1 Updated Aug 6, 2024

  • Abel Public

    Forked from math-comp/Abel

    A proof of Abel-Ruffini theorem.

    Coq Updated Jul 16, 2024

  • deriving Public

    Forked from arthuraa/deriving

    Class instances for Coq inductive types with little boilerplate

    Coq MIT License Updated Apr 23, 2024

  • real-closed Public

    Forked from math-comp/real-closed

    Theorems for Real Closed Fields

    Coq Updated Mar 19, 2024

  • finmap Public

    Forked from math-comp/finmap

    Finite sets, finite maps, multisets and order

    Coq 2 Updated Dec 8, 2023

  • coq Public

    Forked from coq/coq

    Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive develo…

    OCaml GNU Lesser General Public License v2.1 Updated Dec 7, 2023

  • record-expansion Public

    A translation from Coq to Coq expanding and eliminating records (WIP)

    Coq 1 Updated Mar 16, 2023

  • refinement Public

    Forked from QuentinCanu/refinement
    Coq Updated Jan 27, 2023

  • metacoq Public

    Forked from MetaCoq/metacoq

    Metaprogramming in Coq

    Coq MIT License Updated Jan 12, 2023

  • dpt-rp1-py Public

    Forked from janten/dpt-rp1-py

    Python script to manage Sony DPT-RP1 without Digital Paper App

    Python Updated Sep 10, 2022

  • PG Public

    Forked from ProofGeneral/PG

    This repo is the new home of Proof General

    Emacs Lisp GNU General Public License v3.0 Updated Sep 5, 2022

  • sniper Public

    Forked from smtcoq/sniper
    Coq Other Updated Jul 8, 2022

  • trakt Public

    Forked from ecranceMERCE/trakt

    A generic goal preprocessing tool for proof automation tactics in Coq

    Prolog GNU Lesser General Public License v3.0 Updated Jul 6, 2022

  • coq-elpi Public

    Forked from LPCIC/coq-elpi

    Coq plugin embedding elpi

    OCaml GNU Lesser General Public License v2.1 Updated Apr 11, 2022

  • opam-repository Public

    Forked from ocaml/opam-repository

    Main public package repository for OPAM, the source package manager of OCaml.

    OCaml 1 Creative Commons Zero v1.0 Universal Updated Feb 2, 2022

  • CoqEAL Public

    Forked from coq-community/coqeal

    CoqEAL -- The Coq Effective Algebra Library

    Coq Other Updated Dec 15, 2021

  • pygments Public

    Forked from pygments/pygments

    Pygments is a generic syntax highlighter written in Python

    Python BSD 2-Clause "Simplified" License Updated Dec 10, 2021

  • flocq Public

    Fork of https://gitlab.inria.fr/flocq/flocq

    Coq GNU Lesser General Public License v3.0 Updated Nov 5, 2021

  • unicoq Public

    Forked from unicoq/unicoq

    An enhanced unification algorithm for Coq

    OCaml MIT License Updated Oct 30, 2021

  • lemma-overloading Public

    Forked from coq-community/lemma-overloading

    Libraries demonstrating design patterns for programming and proving with canonical structures in Coq [maintainer=@anton-trunov]

    Coq Other Updated Apr 4, 2021

  • fcsl-pcm Public

    Forked from imdea-software/fcsl-pcm

    Partial Commutative Monoids

    Coq Apache License 2.0 Updated Apr 3, 2021

  • analysis Public

    Forked from math-comp/analysis

    Mathematical Components compliant Analysis Library

    Coq Other Updated Mar 27, 2021

  • sandpit Public

    Coq 3 1 Updated Mar 22, 2021

  • Coq-Polyhedra Public

    Forked from Coq-Polyhedra/Coq-Polyhedra

    Formalizing convex polyhedra in Coq

    Coq Other Updated Jan 28, 2021

  • vass Public

    Coq 3 Updated Sep 29, 2020