Skip to content

Instantly share code, notes, and snippets.

View amintimany's full-sized avatar

Amin Timany amintimany

42 followers · 6 following
View GitHub Profile
@amintimany
amintimany / init.el
Last active April 28, 2016 21:24
my emacs init file for coq
(defun load-if-exists (file) "load a file if it exists"
(if (file-exists-p file) (load-file file) ()))
(load-if-exists "~/.emacs.d/ProofGeneral/generic/proof-site.el")
(custom-set-variables
;; custom-set-variables was added by Custom.
;; If you edit it by hand, you could mess it up, so be careful.
;; Your init file should contain only one such instance.
;; If there is more than one, they won't work right.
'(coq-double-hit-enable t)
@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.
@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 / .zshrc
Last active May 1, 2016 14:51
# 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 / app_env_path.md
Created May 1, 2016 14:38

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.

@amintimany
amintimany / printing over ssh
Created July 31, 2017 14:12
cat file.pdf | ssh username@ssh-host 'lp -d destination -'
@amintimany
amintimany / Mac_Unicode_Problem.md
Last active April 28, 2020 09:15

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.

@amintimany
amintimany / talia.v
Created October 10, 2020 17:56
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.
@amintimany
amintimany / andrej.v
Last active April 13, 2021 19:27
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) :=
@amintimany
amintimany / Aczel_sets.v
Created December 11, 2022 13:25
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.