leodemoura

LEAN=/home/leo/projects/lean0.1/build/debug/shell/lean

all : kernel.olean subtype.olean num.olean sum.olean

%.olean : %.lean
	$(LEAN) -n -o $@ $<

kernel.olean : kernel.lean macros.lua tactic.lua
subtype.olean : subtype.lean kernel.olean
num.olean : num.lean subtype.olean

leodemoura

;; =======================================
;; Magit
(require 'magit)
(global-set-key "\C-xg" 'magit-status)
(setq vc-display-status nil)

;; full screen magit-status
(defadvice magit-status (around magit-fullscreen activate)
  (window-configuration-to-register :magit-fullscreen)
  ad-do-it

leodemoura

(tool-bar-mode -1)
(menu-bar-mode -1)
(scroll-bar-mode -1)
(blink-cursor-mode -1)
(column-number-mode 1)
(setq backup-inhibited t)
(global-set-key (kbd "C-x C-b") 'ibuffer)
(defalias 'yes-or-no-p 'y-or-n-p)
(display-time)

leodemoura

;; =======================================
;; Full Screen
(defun toggle-fullscreen (&optional f)
  (interactive)
  (let ((current-value (frame-parameter nil 'fullscreen)))
    (set-frame-parameter nil 'fullscreen
                         (if (equal 'fullboth current-value)
                             (if (boundp 'old-fullscreen) old-fullscreen nil)
                           (progn (setq old-fullscreen current-value)
                                  'fullboth)))))

leodemoura

import logic data.nat

inductive funext [class] : Prop :=
intro : (∀ {A : Type} {B : A → Type} {f g : Π x, B x} (H : ∀ x, f x = g x), f = g) → funext

namespace funext
definition apply [F : funext] : ∀ {A : Type} {B : A → Type} {f g : Π x, B x} (H : ∀ x, f x = g x), f = g :=
rec_on F (λax, ax)
end funext

leodemoura

;; =======================================
;; prevent the compilation buffer from showing up in both frames
;; http://stackoverflow.com/questions/3311577/when-using-two-frames-in-emacs-how-do-i-prevent-the-compilation-buffer-from-sho
(setq-default display-buffer-reuse-frames t)
;; =======================================

leodemoura

definition dcases_on {C : nat → Type} (n : nat) (c₁ : n = 0 → C 0) (c₂ : Πm, n = succ m → C (succ m)) : C n :=
nat.cases_on n
  (λ (H : n = 0), c₁ H)
  (λ (m : nat) (H : n = succ m), c₂ m H) (eq.refl n)

definition fib.F (n : nat) (r : Π (m : nat), m < n → nat) : nat :=
dcases_on n
  (λ (H : n = 0), succ zero)
  (λ (n₁ : nat) (H₁ : n = succ n₁), dcases_on n₁

leodemoura

inductive list (A : Type) : Type :=
nil {} : list A,
cons   : A → list A → list A

inductive lift.{l₁ l₂} (A : Type.{l₁}) : Type.{max l₁ l₂} :=
mk : A → lift A

definition down.{l₁ l₂} {A : Type.{l₁}} (l : lift.{l₁ l₂} A) : A :=
lift.rec_on l (λ a, a)

leodemoura

import algebra.precategory.basic algebra.precategory.morphism
open precategory morphism truncation eq sigma sigma.ops unit

context
parameter {D₀ : Type}
parameter (C  : precategory D₀)
parameter (D₂ : Π ⦃a b c d : D₀⦄ (f : hom a b) (g : hom c d) (h : hom a c) (i : hom b d), Type)
reducible compose

definition comp₁_type : Type :=

leodemoura

import data.list logic
open nat list decidable bool

definition id [reducible] := nat

definition ctx := list (id × Prop)

definition insert (c : ctx) (i : id) (p : Prop) : ctx :=
(i, p) :: c