Skip to content

Instantly share code, notes, and snippets.

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
@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 / 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:
@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
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 / 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.