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
/\ = ∧ | |
\/ = ∨ | |
=> = ⇒ (also → and ⊃) | |
True = ⊤ | |
False = ⊥ | |
!- = ⊢ | |
/\I: X [G], Y [G] !- X /\ Y [G] | |
/\E1: X /\ Y [G] !- X [G] |
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
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); |
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
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 |
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
hard goal => P a <-------- P b <= easy goal | |
^ | |
| | |
| | |
| subst eq P | |
| | |
| | |
| | |
a ========= b | |
eq |
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
suc (a + suc b) == suc (b + suc a) | |
^ | |
| | |
| | |
suc (suc (a + b)) == suc (b + suc a) | |
^ | |
| | |
| | |
suc (suc (a + b)) == suc (suc (b + a)) | |
^ |
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
... = 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) | |
[] |
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
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 |
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
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 |
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
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 | |
.----------------------. | |
| .--------------. | |
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
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> |
OlderNewer