Skip to content

Instantly share code, notes, and snippets.

View anton-trunov's full-sized avatar
🐓
Quickchecking languages implementations...

Anton Trunov anton-trunov

🐓
Quickchecking languages implementations...
View GitHub Profile
@clayrat
clayrat / bove_capretta_ssr.v
Last active June 25, 2022 08:57
Bove-Capretta w/ Equations+SSReflect
(** * The Bove-Capretta method
This method involves building the graph and/or domain of a recursive
definition and to define it by recursion + inversion on that graph,
but not direct pattern matching. We show a difficult example
involving nested recursive calls. *)
From Equations Require Import Equations.
From Coq Require Import ssreflect ssrbool ssrfun.
From mathcomp Require Import ssrnat eqtype.

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
@neel-krishnaswami
neel-krishnaswami / abt
Last active June 15, 2021 21:17
Abstract binding trees implementation
(* -*- 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
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
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 March 29, 2019 18:12
A presentation about coinductive types (given at UPenn's PLClub)
Require Arith.
Require Import List.
Import ListNotations.
(** * Coinductive types and coinduction *)
@UlfNorell
UlfNorell / Fulcrum.agda
Created April 27, 2018 11:04
Challenge 3 of the Great Theorem Prover Showdown
-- 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 (_≤?_)