Instantly share code, notes, and snippets.

tangentstormtangentstorm

• Sort options
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'
Created Jul 30, 2019
View collatz.ijs
 C =: -:`(1+3&*)@.(2&|)"0 R =: -:^:(-.@(2&|))^:_ S =: 1 + 3&* T =: R@([`S@.(2&|))"0 T i. 10
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:
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
Last active Jul 11, 2018
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:›
Created Jun 30, 2018
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)"
Created May 2, 2018
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
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,
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. *
Created May 17, 2017
magic squares in k
View magic-squares.k
 / https://en.wikipedia.org/wiki/Siamese_method msq: {[m] s:(-1+m*m) (1 -1 +)\ (_ m%2; 0); 1+/.[m#,m#0; ; :; ]'[(s+2 -1*/:,/m#/:!m)!m; !#s]}
You can’t perform that action at this time.