NicolasRouquette

-- A basic framework for graph theory on multidigraphs in Lean
-- and a proof that no_watershed_condition is sufficient to
-- establish that a graph has a unique sink for each vertex
--
-- I hope to give some introduction to the syntax of how Lean works here,
-- but I assume some familiarity with functions, pattern matching,
-- type theory, and proofs.
--
-- The most important thing to note is that `begin` and `end` delineate
-- sections of code in "tactic/interactive proof mode" (as opposed to

NicolasRouquette

-----BEGIN PGP PUBLIC KEY BLOCK-----

mQINBFz4QfkBEADka2rH/kSD1vvNvVT9E04N14pRi4s9qg7lu2i4vsXLOKOO49nR
YHCN3DVM1FnPNdkb3kHThvPZh+afTsAzJDa2GG51A+Kfr3+vrZTEBvuCuFFHP8Dd
zUw38csHjWBMex4RQ7Hil6tnuJ3BHKwhC2rmRDjnyv5hYaDhclW1rC8k1yheX4Z7
27jYe0H2M4Gb4BebdtzFZzOI7Iz+1GBCqyZPc/QC8eoVrgzrZ6YkrmmxrqREYQLf
qbze3KGhju+nC/AymrThykvQ54l/myCBcU4BVqJWl0uUsvm5xnQgEUqlnxebI2iC
7lq3KiKhflTqHYhTgcln2y04TDQNJ+/jxOSbM5TKCbMb+WPPSBHNH3XbmsjvmUDs
+yqcWXcodAfhAes9RckTT5EkjAMdfMEbWxLS+6JV3cHetZGlhsRLSVZgqeyCQ1H6
BUrQ8Gbp66+fz45cYlZDnYT/8AZGIx+CjOeTe8IhjNTwhwdYheeMBEvDioFtbtww

NicolasRouquette

Building & Installing Apache Zeppelin 0.8 (from GIT)

Install R

On MacOSX, follow these steps: http://www.reed.edu/data-at-reed/software/R/r_studio.html

• Install R
• Install RStudio
• Download the startup_packages.R script from that page:

NicolasRouquette

package tags

import frameless.{TypedColumn, TypedDataset}
import frameless.ops.SmartProject
import frameless.{CatalystCast, Injection}
import org.apache.spark.SparkConf
import org.apache.spark.sql.SparkSession

import scala.{App,Int}
import scala.Predef.{require,String}

NicolasRouquette

package cafe

import java.lang.{Integer,System}

import fs2._

import scala.{App,Long,StringContext}

object Main1 extends App {

NicolasRouquette

/*
 * Copyright 2016 California Institute of Technology ("Caltech").
 * U.S. Government sponsorship acknowledged.
 *
 * Licensed under the Apache License, Version 2.0 (the "License");
 * you may not use this file except in compliance with the License.
 * You may obtain a copy of the License at
 *
 *     http://www.apache.org/licenses/LICENSE-2.0
 *