Skip to content

Instantly share code, notes, and snippets.

@tangentstorm
tangentstorm / something4thy.js
Created Aug 2, 2013
something 4thy this way comes...
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 },
@tangentstorm
tangentstorm / animation.ijs
Created Aug 12, 2019
Basic animation in J
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 collatz.ijs
C =: -:`(1+3&*)@.(2&|)"0
R =: -:^:(-.@(2&|))^:_
S =: 1 + 3&*
T =: R@([`S@.(2&|))"0
T i. 10
@tangentstorm
tangentstorm / Poly100.thy
Last active Aug 9, 2018
start on a proof of the polyhedron formula
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
@tangentstorm
tangentstorm / failure.thy
Created Aug 1, 2018
how do i do this in isabelle?
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
textA 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
@tangentstorm
tangentstorm / macro.rs
Created Mar 24, 2018
my first rust macro
View macro.rs
fn when(&mut self, v:VID, val:NID, nid:NID)->NID {
macro_rules! op {
[not $x:ident] => {{ let x1 = self.when(v, val, $x); self.not(x1) }};
[$f:ident $x:ident $y:ident] => {{
let x1 = self.when(v, val, $x);
let y1 = self.when(v, val, $y);
self.$f(x1,y1) }}}
if v >= self.vars.len() { nid }
else { match self[nid] {
Op::Var(x) if x==v => val,
@tangentstorm
tangentstorm / risc.pas
Created Apr 9, 2013
RISC virtual machine by Niklaus Wirth from his book, Compiler Construction. (This is actually oberon, not pascal, but github doesn't highlight oberon)
View risc.pas
MODULE RISC; (* NW 22.9.07 / 28.3.11 *)
IMPORT SYSTEM, Texts, Oberon;
CONST
MemSize = 1024; (* in words *)
MOV = 0; AND = 1; IOR = 2; XOR = 3; LSL = 4; ASR = 5;
ADD = 8; SUB = 9; MUL = 10; Div = 11; CMP = 12;
You can’t perform that action at this time.