AndrasKovacs

{-# language Strict, LambdaCase, BlockArguments #-}
{-# options_ghc -Wincomplete-patterns #-}

{-
Minimal demo of "glued" evaluation in the style of Olle Fredriksson:

  https://github.com/ollef/sixty

The main idea is that during elaboration, we need different evaluation

jozefg

Operator Russell : ().
[Russell] =def= [{x : U{i} | not(member(x; x))}].

Tactic break-plus {
  @{ [x : _ + _ |- _] => elim <x> }
}.

Theorem u-in-u-wf : [member(member(U{i}; U{i}); U{i'})] {
  unfold <member>; eq-eq-base; unfold <bunion>; auto;
  csubst [ceq(U{i}; lam(x.snd(x)) pair(inr(<>); U{i}))]

bobatkey

(* This is a demonstration of the use of the SML module system to
   encode (Generalized Algebraic Datatypes) GADTs via Church
   encodings. The basic idea is to use the Church encoding of GADTs in
   System Fomega and translate the System Fomega type into the module
   system. As I demonstrate below, this allows things like the
   singleton type of booleans, and the equality type, to be
   represented.

   This was inspired by Jon Sterling's blog post about encoding proofs
   in the SML module system:

larrytheliquid

open import Data.Nat
open import Data.String
open import Function
open import LabelledTypes
module LabelledAdd1 where

----------------------------------------------------------------------

add : (m n : ℕ) → ⟨ "add" ∙ m ∙ n ∙ ε ∶ ℕ ⟩
add m n = elimℕ (λ m' → ⟨ "add" ∙ m' ∙ n ∙ ε ∶ ℕ ⟩)

copumpkin

module Telescope where

open import Function
open import Data.Unit
open import Data.Product
open import Data.Nat
open import Data.Vec

infixr 6 _∷_

larrytheliquid

(set-fontset-font t '(#x2080 . #x00208e) "Monoco")
(set-fontset-font t '(#x002070 . #x00207e) "Monoco")

copumpkin

{-# OPTIONS --without-K #-}
module Unique where

open import Level
open import Data.Empty
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality

module Unique {a} {A : Set a} (_≟_ : (x y : A) → Dec (x ≡ y)) where
  squish : {x y : A} → x ≡ y → x ≡ y

wearhere

#! /bin/sh

# On alternate invocations, this script 
# saves the path of the source file currently open in Xcode
# and restores the file at that path in Xcode.
#
# By setting Xcode (in Behaviors) to run this script when "Run Starts" 
# and when "Run Completes", you can prevent it from switching to main.m 
# when a run finishes.
# See http://stackoverflow.com/questions/7682277/xcode-4-2-jumps-to-main-m-every-time-after-stopping-simulator 

Machx

samurai% /System/Library/Frameworks/CoreServices.framework/Frameworks/LaunchServices.framework/Support/lsregister -kill -r -domain local -domain system -domain user

stuartcarnie

//
//	main.m
//	ProtectTest
//	Demonstrates newer versions of iOS now support PROT_EXEC pages, for just-in-time compilation.
//
//      Must be compiled with Thumb disabled
//
//	Created by Stuart Carnie on 3/4/11.
//	Copyright 2011 Manomio LLC. All rights reserved.
//