Skip to content

Instantly share code, notes, and snippets.

tangentstorm tangentstorm

Block or report user

Report or block tangentstorm

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
View GitHub Profile
@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;
@tangentstorm
tangentstorm / BeaconTeleport.cs
Created Dec 5, 2017
BeaconTeleport for unity3d / VRTK
View BeaconTeleport.cs
using System.Collections;
using System.Collections.Generic;
using UnityEngine;
using VRTK;
/* This class lets you leave a beacon in the scene and teleport to it later.
*
* It should be attached to an object that also has a VRTK_ControllerEvents
* component attached.
*
You can’t perform that action at this time.