{{ message }}

Instantly share code, notes, and snippets.

# tangentstorm tangentstorm

Last active Jul 11, 2018
View TopSpace.thy
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 (* 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
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 (* 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
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 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
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 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
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 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
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 / 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]}
Created Sep 1, 2016
View learntris.c
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 #include #define I(n) for(int i=0; i
Created Jun 24, 2016
lexer and parser for K language... part of IntelliK
View k.bnf
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters. Learn more about bidirectional Unicode characters
 { parserClass="com.x1010data.intellik.parser.KParser" extends="com.intellij.extapi.psi.ASTWrapperPsiElement" psiClassPrefix="K" psiImplClassSuffix="Impl" psiPackage="com.x1010data.intellik.psi" psiImplPackage="com.x1010data.intellik.psi.impl" elementTypeHolderClass="com.x1010data.intellik.psi.KTypes"
Created Jun 11, 2016
arduino stuff