tangentstorm

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

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'

tangentstorm

C =: -:`(1+3&*)@.(2&|)"0
R =: -:^:(-.@(2&|))^:_
S =: 1 + 3&*
T =: R@([`S@.(2&|))"0
T i. 10

tangentstorm

(* 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

(* 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

(* 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:›

tangentstorm

(* 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)"

tangentstorm

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

  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

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;