View meld.js
glue = (x,y) => x === undefined ? y : Array.isArray(x) ? x.concat(y) : [x,y] | |
function meld(xs) { | |
let idx = {}, res = [], it | |
for (x of xs) { | |
if (x.id in idx) it = res[idx[x.id]] | |
else { it = {id: x.id}; idx[x.id] = res.length; res.push(it) } | |
for (k of Object.keys(x)) if (k!=='id') it[k] = glue(it[k], x[k]) } | |
return res } |
View animation.ijs
NB. Code from the "Basic Animation In J" video | |
NB. https://www.youtube.com/watch?v=uL-70fMTVnw | |
NB. ------------------------------------------------------------------------ | |
NB. animation demo | |
load 'viewmat' | |
coinsert'jgl2' | |
wd 'pc w0 closeok' NB. parent control (window) named 'w0' |
View catalan-1-filter.ijs
c =: '01' ([: +/ =)"0 _ ] NB. count 0 and 1 | |
t =: {{(*/ <:/"1 c\ y) *. =/c y }} NB. the two rules | |
g =: {{'01' {~ #:i.2^2*y}} NB. generate the numbers | |
f =: {{y {~ I.t"1 y}} NB. filter by t | |
f g 3 |
View something4thy.js
var b4 = (new function() { var EOF='\0',self = { | |
d:[], a:[], // data and auxiliary/return stack | |
defs:[],core:[],scope:[], // dictionary | |
base:10, // numbers | |
cp:-1, ch:'\x01',ibuf:[],wd:'', // lexer state | |
compiling:false,state:[],target:[], // compiler state | |
def : function (k,v){ | |
var res=self.defs.length; self.defs.push(v); self.scope[0].push([k,res]); return res }, |
View collatz.ijs
C =: -:`(1+3&*)@.(2&|)"0 | |
R =: -:^:(-.@(2&|))^:_ | |
S =: 1 + 3&* | |
T =: R@([`S@.(2&|))"0 | |
T i. 10 |
View Poly100.thy
(* Isar Proofs (eventually) for three theorems from http://www.cs.ru.nl/~freek/100/ | |
#13 Polyhedron Formula (F + V - E = 2) | |
#50 The Number of Platonic Solids | |
#92 Pick's theorem | |
*) | |
theory Poly100 | |
imports Main "HOL.Binomial" "HOL-Analysis.Polytope" | |
begin |
View failure.thy
(* how do i do this?? *) | |
function simplex_count :: "int⇒int⇒int" where | |
"simplex_count 0 0 = 1" | | |
"simplex_count 0 1 = 0" | | |
"simplex_count 1 0 = 2" | | |
"simplex_count n k = (simplex_count (n-1) k + simplex_count n (k-1))" | |
sorry | |
lemma simplex_count_lemma: |
View TopSpace.thy
(* Topological Spaces | |
Based on "A Bridge to Advanced Mathematics" by Dennis Sentilles | |
Translated to Isar by Michal J Wallace *) | |
theory TopSpace | |
imports Main | |
begin | |
text ‹A topological space (X,T) is a pair where X is a set whose elements | |
are called the "points" of the topological space, and T is a fixed collection of | |
subsets of X called neighborhoods, with the following properties:› |
View MJWGroups.thy
(* Simple Group Theory from Scratch *) | |
theory MJWGroups | |
imports Pure | |
begin | |
locale group = | |
fixes op :: "'g ⇒ 'g ⇒ 'g" (infixl "∘" 65) | |
fixes id :: "'g" ("𝔦") | |
fixes inv :: "'g ⇒ 'g" | |
assumes assoc: "(a ∘ b) ∘ c == a ∘ (b ∘ c)" |
View magic-eye.ijs
dw =. 10 | |
dw2 =. dw | |
hw =. 5 50 | |
tl =. '..' ((-,+)/>.-:dw2,~{:hw) } 40 # ' ' | |
bg0 =. hw $ a.i.'.' | |
bg1 =. 26 | (]+ ] = dw |. ]) hw $? (*/hw)#26 | |
bg1 =. 65 + bg1 | |
bg =. a. {~ bg1 | |
el =. "_1 _ | |
lf =. 15 |
NewerOlder