Skip to content

Instantly share code, notes, and snippets.

Avatar
🐓
Hacking Coq

Anton Trunov anton-trunov

🐓
Hacking Coq
View GitHub Profile
View gccemacs-macos.org

Emacs 28 native-comp experiment

  • Reinstall regular gcc without libgccjit
# https:/stackoverflow.com/questions/9369519/reset-homebrew-formula/
# Revert to original gcc.rb
brew update-reset
# Check languages for the absence of jit
brew edit gcc
# Reinstall regular gcc
brew reinstall gcc
View ssreflect.v
Require Import ssreflect.
(*
Playing with
https://coq.inria.fr/refman/proof-engine/ssreflect-proof-language.html#type-families
*)
Lemma foo {a1 a2} : a1 = a2 -> a1 + a1 = a2 + a2.
Fail progress case.
(* Either one works, and gives a goal that can be dispatches by reflexivity. *)
@Lysxia
Lysxia / coinduction.v
Created Mar 29, 2019
A presentation about coinductive types (given at UPenn's PLClub)
View coinduction.v
Require Arith.
Require Import List.
Import ListNotations.
(** * Coinductive types and coinduction *)
@UlfNorell
UlfNorell / Fulcrum.agda
Created Apr 27, 2018
Challenge 3 of the Great Theorem Prover Showdown
View Fulcrum.agda
-- Problem 3 of @Hillelogram's Great Theorem Prover Showdown.
-- https://www.hillelwayne.com/post/theorem-prover-showdown
--
-- Implemented using current stable-2.5 branch of Agda
-- (https://github.com/agda/agda/tree/08664ac) and the agda-prelude
-- library (https://github.com/UlfNorell/agda-prelude/tree/d193a94).
module Fulcrum where
open import Prelude hiding (_≤?_)
View inj2.lean
open eq
inductive I (F : Type₁ → Prop) : Type₁ :=
mk : I F
axiom InjI : ∀ {x y}, I x = I y → x = y
definition P (x : Type₁) : Prop := ∃ a, I a = x ∧ (a x → false).
definition p := I P
@neel-krishnaswami
neel-krishnaswami / abt
Last active Jun 15, 2021
Abstract binding trees implementation
View abt
(* -*- mode: ocaml; -*- *)
module type FUNCTOR = sig
type 'a t
val map : ('a -> 'b) -> 'a t -> 'b t
end
type 'a monoid = {unit : 'a ; join : 'a -> 'a -> 'a}
type var = string