Skip to content
View gmalecha's full-sized avatar

Organizations

@coq-ext-lib

Block or report gmalecha

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
  • coq.github.io Public

    Forked from coq/coq.github.io

    Source files of the coq.inria.fr website

    HTML Other Updated Nov 11, 2024
  • A rosetta stone for metaprogramming in Coq, with different examples of tactics, plugins, etc implemented in different metaprogramming languages [maintainer=@yforster]

    Coq MIT License Updated Jun 30, 2023
  • llvm-project Public

    Forked from llvm/llvm-project

    The LLVM Project is a collection of modular and reusable compiler and toolchain technologies. Note: the repository does not accept github pull requests at this moment. Please submit your patches at…

    Other Updated Jan 1, 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 Oct 1, 2022
  • rouge Public

    Forked from rouge-ruby/rouge

    A pure-ruby code highlighter that is compatible with pygments http://rouge.jneen.net/

    Ruby Other Updated Sep 9, 2022
  • nixos-weekly Public

    Forked from NixOS/nixos-weekly

    NixOS Weekly Newsletter

    HTML Creative Commons Attribution Share Alike 4.0 International Updated Mar 26, 2021
  • opam-coq-archive Public

    Forked from coq/opam

    Archive for all Coq related OPAM packages organized in various repositories

    JavaScript 1 GNU Lesser General Public License v2.1 Updated Sep 24, 2020
  • website

    JavaScript Apache License 2.0 Updated Jul 5, 2020
  • Invoke SMT solvers from Coq to check obligations

    OCaml 10 3 MIT License Updated Jun 16, 2020
  • Access hint databases from tactics.

    Coq 12 3 MIT License Updated Apr 22, 2020
  • coq-printf Public

    Implementation of sprintf for Coq

    Coq 18 2 MIT License Updated Apr 6, 2020
  • coq-apply-any Public archive

    An extension to eauto that allows you to apply an arbitrary lemma from a hint database

    OCaml 1 Updated Dec 4, 2019
  • ceps Public

    Forked from coq/rfcs

    Coq Enhancement Proposals

    Updated Nov 28, 2019
  • mirror-core Public

    A framework for extensible, reflective decision procedures.

    Coq 19 5 Other Updated Nov 25, 2019
  • coq-seal Public

    Implementation of sealing in Coq with macros for generation

    Coq 1 MIT License Updated Sep 26, 2019
  • template-coq Public

    Forked from MetaCoq/metacoq

    Reflection library for Coq

    OCaml 12 MIT License Updated Sep 26, 2019
  • Implementation of extensible records in Coq

    Coq 6 1 MIT License Updated Aug 16, 2019
  • coq-k Public

    Some formalization of the K framework in Coq

    Coq 2 Updated Aug 3, 2019
  • SquiggleEq Public

    Forked from aa755/SquiggleEq
    Coq MIT License Updated Jun 27, 2019
  • clang Public

    Forked from llvm-mirror/clang

    Mirror of official clang git repository located at http://llvm.org/git/clang. Updated every five minutes.

    C++ Other Updated Mar 13, 2019
  • Useful utility functions for writing Coq plugins

    OCaml 4 1 MIT License Updated Mar 2, 2019
  • Formalization of the Interaction Tree Datatype in Coq

    Coq MIT License Updated Jan 17, 2019
  • bbv Public

    Forked from mit-plv/bbv

    Bedrock Bit Vector Library

    Coq MIT License Updated Aug 1, 2018
  • Co-inductive interaction trees provide a way to represent (potentially) non-terminating programs with I/O behavior.

    Coq 17 1 Updated Jul 9, 2018
  • row-types Public

    Forked from target/row-types
    Haskell MIT License Updated Mar 20, 2018
  • A formalization of category theory in Coq for personal study and practical work

    Coq Updated Mar 18, 2018
  • fraxl Public

    Forked from ElvishJerricco/fraxl
    Haskell BSD 3-Clause "New" or "Revised" License Updated Feb 12, 2018
  • Composable, streaming, and efficient left folds

    Haskell BSD 3-Clause "New" or "Revised" License Updated Jan 18, 2018
  • CTRex.hs Public

    Forked from strake/CTRex.hs

    Open records for Haskell

    Haskell Other Updated Aug 24, 2017
  • Aeson instances for CTRex records

    Haskell BSD 3-Clause "New" or "Revised" License Updated Aug 24, 2017