jonsterling

ac

Goal:

◊ ≫
  ∩(U<0>; A.
  ∩(U<0>; B.
  ∩(∏(A; _.∏(B; _.U<0>)); Q.
 ∏(∏(A; a.prod(B; b.ap(ap(Q; a); b))); _.

jonsterling

%solve 
ctx/snoc (ctx/snoc ctx/nil (! ↑ unit)) (@ ([x:tm] ! ↑ unit))
   >> judgement/type (@ ([x:tm] @ ([y:tm] ! ↑ unit))).
 OK
- :
   ctx/snoc (ctx/snoc ctx/nil (! ↑ unit)) (@ ([x:tm] ! ↑ unit))
      >> judgement/type (@ ([x:tm] @ ([y:tm] ! ↑ unit)))
   = >>/,
        ([x:tm] [x':otm (ctx/snoc ctx/nil (! ↑ unit))]
            [x1:weaken (ctx/snoc ctx/nil (! ↑ unit)) x x'] [y:tm]

jonsterling

val : type.
exp : type.

set : val.
void : val.
unit : val.
& : exp -> exp -> val.   %infix right 10 &.
+ : exp -> exp -> val.   %infix right 10 +.

ax : val.

jonsterling

record Container : Set where
  constructor _▹_
  field
    sh : Set
    po : sh → Set

⟦_⟧ : Container → Set → Set
⟦ sh ▹ po ⟧ A = Σ[ s ∶ sh ] (po s → A)

module _ {A : Set} {C : Container} (Q : A → Set) where

jonsterling

tp : type.

val : tp -> type.
el : tp -> type.
! : val A -> el A.

eq : {A:tp} el A -> el A -> type.

⇓ : el A -> val A -> type. %infix right 11 ⇓.
red : eq A M (! N)

jonsterling

Keybase proof

I hereby claim:

• I am jonsterling on github.
• I am jonsterling (https://keybase.io/jonsterling) on keybase.
• I have a public key whose fingerprint is 0D26 4B16 F650 0D8A CFB1 A781 2FC8 9E5C B6AC C521

To claim this, I am signing this object:

jonsterling

Require Import Coq.Unicode.Utf8.
Require Import List.

Global Obligation Tactic := compute; firstorder.

(* How do to topology in Coq if you are secretly an HOL fan.
   We will not use type classes or canonical structures because they
   count as "advanced" technology. But we will use notations.
 *)

jonsterling

(* It is not possible in Standard ML to construct an identity type (or any other
 * indexed type), but that does not stop us from speculating. We can specify with
 * a signature equality should mean, and then use a functor to say, "If there
 * were a such thing as equality, then we could prove these things with it."
 * Likewise, we can use the same trick to define the booleans and their
 * induction principle at the type-level, and speculate what proofs we could
 * make if we indeed had the booleans and their induction principle.
 *
 * Functions may be defined by asserting their inputs and outputs as
 * propositional equalities in a signature; these "functions" do not compute,

jonsterling

// A nice little example of using transactional signal generators.
// Imagine a board of buttons with numbers on it, and a big red button with a picture of a bomb on it.
// When a button with a number is pressed, `increment` is invoked with that number. When the bomb
// button is pressed, then `reset` is invoked.
//
//This returns a signal of the running total made by incrementing by numbers and resetting by explosions.
RACDynamicSignalGenerator *increment = [[RACDynamicSignalGenerator alloc] initWithBlock:^RACSignal *(NSNumber *add) {
	return [RACSignal return:^(NSNumber *count) {
		return @(count.integerValue + add.integerValue);
	}];

jonsterling

module type TYPE = sig
  type t
end

module type EMPTY = functor (T : TYPE) -> sig
  val apply : T.t
end

type empty = (module EMPTY)