Skip to content

Instantly share code, notes, and snippets.

_∘_ : ∀ {α β γ}
→ {A : Set α} {B : A → Set β} {C : {x : A} → B x → Set γ}
→ (f : {x : A} → (y : B x) → C y)
→ (g : (x : A) → B x)
→ ((x : A) → C (g x))
(f ∘ g) x = f (g x)
_∘′_ : ∀ {α β γ}
→ {A : Set α} {B : Set β} {C : Set γ}
→ (B → C) → (A → B) → (A → C)
module filter where
data Bool : Set where
true false : Bool
data List (A : Set) : Set where
[] : List A
_::_ : A → List A → List A
infix 4 _≡_
data _≡_ {A : Set} (x : A) : A → Set where
@DreamLinuxer
DreamLinuxer / c-num.scm
Last active December 19, 2015 23:49
Church numeral
(define zero (lambda (f) (lambda (x) x)))
(define (add-1 n)
(lambda (f) (lambda (x) (f ((n f) x)))))
; n := apply f to x n times
(define one (lambda (f) (lambda (x) (f x))))
(define two (lambda (f) (lambda (x) (f (f x)))))
(define (add a b)
(lambda (f) (lambda (x)
@DreamLinuxer
DreamLinuxer / debug.log
Created November 15, 2012 08:09
GDB script example
Reading symbols from ~/gist/gist-4077328/gdb_test...done.
Breakpoint 1 at 0x4005cf: file gdb_test.c, line 7.
Breakpoint 1, output (val=91652772) at gdb_test.c:7
7 printf("OUTPUT: %X\n",val);
#0 output (val=91652772) at gdb_test.c:7
#1 0x0000000000400632 in rand_output (prev=4294967295, mid=1073741824, mask=2147483647) at gdb_test.c:16
#2 0x000000000040066a in main () at gdb_test.c:23
Breakpoint 1, output (val=4481602) at gdb_test.c:7
@DreamLinuxer
DreamLinuxer / self_rep.c
Created November 15, 2012 02:21
self reproduce maker
char s[]={109,97,105,110,40,41,10,123,10,105,110,116,32,105,59,10,112,114,105,110,116,102,40,34,99,104,97,114,32,115,91,93,61,123,34,41,59,10,102,111,114,40,105,61,48,59,115,91,105,93,59,43,43,105,41,112,114,105,110,116,102,40,34,37,100,44,34,44,115,91,105,93,41,59,10,112,114,105,110,116,102,40,34,48,125,59,37,99,34,44,49,48,41,59,10,112,114,105,110,116,102,40,34,37,115,34,44,115,41,59,10,125,0};
main()
{
int i;
printf("char s[]={");
for(i=0;s[i];++i)printf("%d,",s[i]);
printf("0};%c",10);
printf("%s",s);
}