Skip to content

Instantly share code, notes, and snippets.

View amintimany's full-sized avatar

Amin Timany amintimany

View GitHub Profile
From stdpp Require Import list.
From iris.algebra Require Import excl numbers gmap.
From iris.base_logic Require Export invariants saved_prop.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang proofmode notation.
(* move *)
Lemma list_sum_replicate n m : list_sum (replicate n m) = n * m.
Proof.
revert m; induction n as [|n IHn]; first done; intros ?; rewrite /= IHn; lia.
From Coq.Classes Require Import RelationClasses Morphisms.
From Coq.Setoids Require Import Setoid.
Inductive Ens : Type :=
ens_intro : forall A : Type, (A -> Ens) -> Ens.
Definition idx (A : Ens) : Type := match A with ens_intro T _ => T end.
Definition elem (A : Ens) (i : idx A) : Ens :=
match A as u return idx u -> Ens with ens_intro B f => fun j => f j end i.
From Coq.Unicode Require Import Utf8.
From Coq.Program Require Import Tactics.
Record Tomega := {
yes : nat → Prop;
no : nat → Prop;
disjoint : ∀ n, ¬ (yes n ∧ no n)
}.
Definition leq (x y : Tomega) :=
Require Import Coq.Program.Tactics.
(* Require Import Ornamental.Ornaments. *)
(* Set DEVOID lift type. *)
Parameter A : Type.
Parameter B : Type.
Parameter f : A -> B.
Parameter g : B -> A.

Unicode problems on Mac

For some reason OSX lacks fonts to show latin subscript fonts. The machine you are viewing this document on has this issue if you cannot view the following string properly (it should consist of two characters representing subscript t, and l letters): "ₜₗ".

To fix, download and install the quivira font, symbola font, and open-sauce-one.

cat file.pdf | ssh username@ssh-host 'lp -d destination -'

usually

launchctl setenv PATH <newpath>

should work. But due to some bug in newer versions of OSX (10.11 or higher) it doesn't. For these versions of OSX

sudo launchctl config user path <new path>

works.

# Path to your oh-my-zsh installation.
export ZSH=/Users/amin/.oh-my-zsh
# Set name of the theme to load.
# Look in ~/.oh-my-zsh/themes/
# Optionally, if you set this to "random", it'll load a random theme each
# time that oh-my-zsh is loaded.
ZSH_THEME="agnoster"
# Uncomment the following line to use case-sensitive completion.
@amintimany
amintimany / CollapseToSet.v
Created July 14, 2015 11:01
This is an example of Coq collapsing any universe level i to Set when we have a constraint of the form Set <= i.
Set Universe Polymorphism.
Set Printing Universes.
Record X : Type :=
{
A : Type;
x : A
}.
Definition untt := {|A := unit; x := tt|}.
@amintimany
amintimany / EqFacts.v
Last active December 10, 2021 00:02
Facts stating equivalence of axioms K, URIP, UIP, eq_rect_eq, projT_2_eq and JMeq_eq in Coq.
Require Import Coq.Logic.JMeq.
Definition JMeq_eq := forall (A : Type) (x y : A), JMeq x y -> x = y.
Section Eq_Facts.
Variable A : Type.
Definition K := forall (x : A) (P : x = x -> Prop), P eq_refl -> forall (eq : x = x), P eq.
Definition URIP := forall (x : A) (eq : x = x), eq = eq_refl.