BekaValentine

def rayHit(raySeg, polys):
  return minimizeBy([rayIntersectsPoly(raySeg, poly) for poly in polys], lambda(pt => length(pt - raySeg)))

def rayIntersectsPoly(raySeg, poly):
  return minimizeBy([rayIntersectsEdge(raySeg, edge) for edge in poly], lambda(pt => length(pt - raySeg)))

def rayIntersectsEdge(raySeg, edgeSeg):
  pt = intersectLines(raySeg, edgeSeg)
  if lineSegmentContains(edgeSeg, pt) && pointIsInRightDir(raySeg, pt)
  then return pt

BekaValentine

hard goal =>   P a <-------- P b   <= easy goal
                       ^
                       |
                       |
                       | subst eq P
                       |
                       |
                       |
                 a ========= b
                       eq

BekaValentine

suc (a + suc b)   == suc (b + suc a)
        ^
        |
        |
suc (suc (a + b)) == suc (b + suc a)
                             ^
                             |
                             |
suc (suc (a + b)) == suc (suc (b + a))
                   ^

BekaValentine

... = begin
        suc (a + suc b)
      ==< cong suc (lemma2 a b) >
        suc (suc (a + b))
      ==< cong (suc.suc) (comm a b) >
        suc (suc (b + a))
      ==< cong suc (sym (lemma2 b a)) >
        suc (b + suc a)
      []

BekaValentine

args \ env size | 1
----------------|---------------------------------------------------------------
  1             | \f x a -> f a (x a)                  =  ap
----------------|---------------------------------------------------------------
  2             | \f x y a -> f a (x a) (y a)          =  (ap .) . ap
----------------|---------------------------------------------------------------
  3             | \f x y z a -> f a (x a) (y a) (z a)  =  (((ap .) . ap) .) . ap


args \ env size | 2

BekaValentine

augur> now, the last piece of phase 1:
augur> well, let me first be precise now about function application:
augur> if    Γ ⊢ M : a → b    and    Γ ⊢ N : a    then    Γ ⊢ M(N) : b
augur> ok now, the last thing we have to worry abot:
augur> if    Γ, x : a ⊢ M : b    then    Γ ⊢ λx:a.M : a → b
augur> this is called lambda abstraction
augur> it just says: if M : b, relying on a variable x : a, then we can use up that variable and get a function out instead
augur> for instance:   x : e ⊢ Dog(x) : prop    so    ⊢ λx:e. Dog(x) : e → prop
augur> or for example:
augur> φ : prop, ψ : prop ⊢ φ ∧ ψ : prop    so    ⊢ λφ:prop. λψ:prop. φ ∧ ψ : prop → prop → prop

BekaValentine

this is the rat that ate the malt that lay in the house that jack built

    .--.   .--.   .------.
    v  |   v  |   v      |
S V O+[_ V O+[_ V O+[S V _]]]

this is the rat that the malt that the house contained was eat by

    .----------------------.
    |  .--------------.    |

BekaValentine

The structure of the sentences is as follows:

  <sentence>
    - <possible meaning for sentence>

please mark each possible meaning with Y if the sentence can have that meaning,
N if the sentence cannot have that meaning, or ? if its unclear, as in

  <sentence>
    - Y <possible meaning>

BekaValentine

    data IntList = nil | cons(int,IntList)

is sugar for

    enum IntListCon { nilCon , consCon };
    struct IntList { IntListCon con ; int head ; IntList* tail; };

    struct IntList nil;
    nil.con = nilCon;

BekaValentine

Left rules are funky: they don't apply to the connective variable as an argument,
instead they introduce syntax that has the variable as an index. You get a kind
of continuation syntax rather than an applicative syntax.





----------------- ID
G, x : A => x : A