View safetraversal.v
Require Import Coq.Init.Nat.
Require Import Coq.Strings.String.
Require Import Coq.Vectors.VectorDef.
Open Scope string_scope.
Open Scope nat_scope.
(* Traversal definition and methods *)
View .sbtrc
# SESSION4-SPARK
# ALL
alias test-sparkintro=;testOnly org.hablapps.sparkintro.test.*
# SECTIONS
alias sparkintro-intro=;testOnly org.hablapps.sparkintro.templates.Intro
alias sparkintro-core=;testOnly org.hablapps.sparkintro.templates.CoreRDDs
View preview-set.txt
Affine
======
pre1 : A -> B + 1
set1 : A x B -> A
pre2 : B -> C + 1
set2 : B x C -> B
View induction.v
Fixpoint times2 (n : nat) : nat :=
match n with
| 0 => 0
| S n => S (S (times2 n))
end.
Fixpoint even (n : nat) : bool :=
match n with
| 0 => true
| S n => negb (even n)
View AffineSetoid.v
Require Import Coq.Logic.FunctionalExtensionality.
Require Import Coq.Setoids.Setoid.
Require Import Coq.Classes.Morphisms.
Generalizable All Variables.
(* Subrelations to enable [setoid_rewrite] in general settings *)
Instance pointwise_eq_ext {A B : Type} `(sb : subrelation B RB eq)
: subrelation (pointwise_relation A RB) eq.
View Monoid.v
Require Import Coq.Logic.FunctionalExtensionality.
Require Import Coq.Setoids.Setoid.
Require Import Coq.Classes.Morphisms.
Generalizable All Variables.
Class Monoid (m : Type) :=
{ mzero : m
; mappend : m -> m -> m
}.
View University.scala
package org.hablapps
package university
import scalaz._, Scalaz._
case class University(name: String, departs: Map[String, Department])
case class Department(budget: Double)
object UniversityManyDep extends App {
View Lens.v
(* Lens and compose definitions *)
Record lens (S A : Type) := {
get : S -> A;
put : S -> A -> S }.
Definition compose {S A B : Type} (ln1 : lens S A) (ln2 : lens A B) : lens S B :=
{| get := fun (s : S) => ln2.(get A B) (ln1.(get S A) s);
put := fun (s : S) (b : B) => ln1.(put S A) s (ln2.(put A B) (ln1.(get S A) s) b) |}.
View LensComposition.md

Lens Composition Proofs

Structure

type Lens s a = (GET :: s -> a, PUT :: s -> a -> s)

Lens Laws

  • GetPut: PUT s (GET s) => s
  • PutGet: GET (PUT s a) => a
View ITraversal.scala
package monocle
import scalaz._, Scalaz._
import Indexable._
abstract class IPTraversal[I, S, T, A, B] {
def modifyF[
F[_]: Applicative,