Documentation

Fad.Assignment02

source
def Assignment02.snoc {α : Type} :
List α → α → List α
Equations
Instances For
    source
    def Assignment02.sum :
    List Nat → Nat
    Equations
    Instances For
      source
      theorem Assignment02.sum_snoc (ms : List Nat) (n : Nat) :
      sum (snoc ms n) = n + sum ms
      source
      theorem Assignment02.foldr_append {α : Type u_1} {β : Type u_2} (f : α → β → β) (e : β) (xs ys : List α) :
      List.foldr f e (xs ++ ys) = List.foldr f (List.foldr f e ys) xs
      source
      theorem Assignment02.sum_append (ms ns : List Nat) :
      sum (ms ++ ns) = sum ms + sum ns
      source
      theorem Assignment02.snoc_eq_append (xs : List Nat) (x : Nat) :
      snoc xs x = xs ++ [x]
      source
      theorem Assignment02.sum_cons (n : Nat) (ns : List Nat) :
      sum (n :: ns) = n + sum ns
      source
      theorem Assignment02.sum_reverse (ns : List Nat) :
      sum ns.reverse = sum ns
      source
      theorem Assignment02.map_id {a : Type} (xs : List a) :
      List.map (fun (x : a) => x) xs = xs
      source
      theorem Assignment02.map_map {a b c : Type} (xs : List a) (f : a → b) (g : b → c) :
      List.map (fun (x : a) => g (f x)) xs = List.map g (List.map f xs)
      source
      inductive Assignment02.AExp :
      Type
      Instances For
        source
        def Assignment02.eval (env : String → Int) :
        AExp → Int
        Equations
        Instances For
          source
          def Assignment02.someEnv :
          String → Int
          Equations
          Instances For
            source
            def Assignment02.simplify :
            AExp → AExp
            Equations
            Instances For
              source
              theorem Assignment02.simplify_correct (env : String → Int) (e : AExp) :
              eval env (simplify e) = eval env e