etosch

# FERPA-protected enrollment status

Your enrollment in this course is protected under FERPA. 

You may choose to earn points by submitting blog posts via Github. 
If you choose to submit blog posts via Github and do so using an account 
that releases personally identifying information, your status as a 
student in this course may become discoverable. 

By accepting this consent form you are accepting responsibility for

etosch

Require Import List.
Require Import EqNat.

Definition alist := list (nat * bool).

Fixpoint in_assignment n (a : alist) : Prop :=
  match a with
    | nil => False
    | (h,_)::t => if beq_nat n h
                  then True

etosch

(defn get-dag
    [blockList]
    "Takes in a list of Blocks; returns a list of lists of Blocks."
    (if (empty? blockList)
        '(())
        (let [^Block this-block (first blockList)]
            (if-let [branchMap (and (.branchQ this-block) (.branchMap (.branchQ this-block)))]
                (let [dests (set (vals branchMap))
                      blists (map (fn [^Block b] (drop-while #(not= % b) blockList)) (seq dests))]
                    (map #(flatten (cons this-block %)) (map get-dag blists))

etosch

function depth
    input : A survey block
    output : integer indicating depth
begin
    idArray <- block id as an array
    return length(idArray)
end

etosch

sm.showBreakoffNotice = function () {
    sm.showFirstQuestion();
};
sm.showBreakoffNotice();

etosch

.breakoff {
    white-space : nowrap;
    display : block;
    position : relative;
    top : 10px;
    left : 20px;
}

etosch

var oldShowQuestion = sm.showQuestion;
var oldRegisterAndShowNextQuestion = sm.registerAndShowNextQuestion;
var addTimingInfo = function(q, tag) {
  var start = document.createElement('input');
  start.type='text';
  start.id=tag+'_'+q.id;
  start.name=tag+'_'+q.id;
  start.form='mturk_form';
  start.hidden=true;
  start.defaultValue=new Date().getTime();

etosch

.answer {
    white-space : nowrap;
    display : block;
}

label {
    display : block;
    padding : 2px 1em 0 0;
    white-space : nowrap;
}

etosch

(* Exercise: 4 stars, recommended (binary)                                                                                                                              
Consider a different, more efficient representation of natural numbers using a binary                                                                                   
rather than unary system. That is, instead of saying that each natural number is either                                                                                 
zero or the successor of a natural number, we can say that each binary number is either                                                                                 
                                                                                                                                                                        
    zero,                                                                                                                                                               
    twice 

etosch

(* There is a short solution to the next exercise. 
If you find yourself getting tangled up, step back and try to look for a simpler way. *)

Theorem app_ass4 :  forall l1 l2 l3 l4 : natlist,
  l1 ++ (l2 ++ (l3 ++ l4)) = ((l1 ++ l2) ++ l3) ++ l4.
Proof.
  intros l1 l2 l3 l4.
  Theorem app_right : forall l1 l2 l3 : natlist,
  l1 ++ (l2 ++ l3) = (l1 ++ l2) ++ l3.
  Proof.