BekaValentine

darryl-mcadamss-macbook-pro:~ darryl$ ls -l /opt/local/bin
total 20096
-rwxr-xr-x  2 root  wheel    18489 Jul 18  2008 autopoint
-rwxr-xr-x  2 root  wheel      331 May 31  2008 bdftops
-rwxr-xr-x  2 root  wheel    18672 Mar 30  2010 bmp2tiff
-rwxr-xr-x  2 root  admin     3656 Oct 26 19:51 c_rehash
lrwxr-xr-x  1 root  admin        3 Mar 16 12:45 captoinfo -> tic
-rwxr-xr-x  1 root  admin    31296 Feb 23  2010 cjpeg
-rwxr-xr-x  1 root  admin    12684 Feb  7  2010 clear
-r-xr-xr-x  1 root  wheel    73852 Jan  1  2010 daemondo

BekaValentine

! Package array Error:  Illegal pream-token (\ensuremath): `c' used.

See the array package documentation for explanation.
Type  H <return>  for immediate help.
 ...                                              
                                                  
l.336 ...r}{\ensuremath{\V{c}}c\ensuremath{\V{c}}}
                                                  
? 

BekaValentine

\documentclass[11pt]{article}

%%%%       %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% LAGDA %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%       %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\usepackage{amssymb, amsmath, tikz-qtree}

%include agda.fmt
%include polycode.fmt

BekaValentine

Comparatives and equatives let you delete the verb, as well as leave it behind, in the secondary clause:

  1. John can [jump] as high as Susan can [----] far
  2. John can [jump] as high as Susan can [jump] far
  3. John can [jump] higher than Susan can [----] far
  4. John can [jump] higher than Susan can [jump] far

But "is Adj" and "is NP" don't, unless it's different:

  5.  John is as [tall] as Susan is [----]

BekaValentine

-- how can we pull out an element from a structure? one approach is zippers.

data PairContext a b = InFst b | InSnd a

data PairZipper a b c = PairZipper c (PairContext a b)

lookFst :: (a,b) -> PairZipper a b a
lookFst (a,b) = PairZipper a (InFst b)

unzipFst :: PairZipper a b a -> (a,b)

BekaValentine

- (void)newDocument:(id)sender {
  NSLog(@"creating document");
  
  NSWindow* newWindow = [[NSWindow alloc]
                         initWithContentRect: NSMakeRect(100,100,500,500)
                         styleMask: NSTitledWindowMask | NSClosableWindowMask | NSResizableWindowMask
                         backing: NSBackingStoreBuffered
                         defer: NO];
  
  [[newWindow contentView] setAutoresizesSubviews: YES];

BekaValentine

uncong-suc : ∀ {m n} → suc m ≡ suc n → m ≡ n
uncong-suc refl = refl

lemma-+drop : ∀ n m o → o + n ≡ o + m → n ≡ m
lemma-+drop n m zero eq = eq
lemma-+drop n m (suc o) eq = {!!}

BekaValentine

we introduce type variables and require the satisfaction of type substitution as usual.

new judgments:

  A functor a   - type A is functorial in variable a

using type contexts D, we introduce some new basic inference rules for functoriality:

     D, a type !- tyctx
  ------------------------ (type variables are functorial in themselves: identity functor)

BekaValentine

/\ = ∧
\/ = ∨
=> = ⇒ (also → and ⊃)
True = ⊤
False = ⊥
!- = ⊢

/\I:      X [G], Y [G] !- X /\ Y [G]

/\E1:     X /\ Y [G] !- X [G]

BekaValentine

foreach edge in poly {
  guard intersectionPoint = intersects(lineFromSegment(edge), lineFromSegment(ray));
  guard sameDirection(intersectionPoint, ray);
  guard withinSegment(intersectionPoint, edge);
  polyIntersectionPoints.push(intersectionPoint);
}

theOneTruePoint = polyIntersectPoints.findClosestTo(rayCastOrigin);