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:
%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] |
val : type. | |
exp : type. | |
set : val. | |
void : val. | |
unit : val. | |
& : exp -> exp -> val. %infix right 10 &. | |
+ : exp -> exp -> val. %infix right 10 +. | |
ax : val. |
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 |
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) |
I hereby claim:
To claim this, I am signing this object:
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. | |
*) |
(* 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, |
// 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); | |
}]; |
module type TYPE = sig | |
type t | |
end | |
module type EMPTY = functor (T : TYPE) -> sig | |
val apply : T.t | |
end | |
type empty = (module EMPTY) |
RACCommand *example = [[RACCommand alloc] initWithSignalBlock:^(id input) { | |
return [RACSignal createWithBlock:^(id<RACSubscriber> subscriber){ | |
[subscriber sendCompleted]; | |
return nil; | |
}]; | |
]; | |
// Now, how will I know when each task has completed? | |
// I certainly cannot tell from `example.executionSignals.flatten`. |