pgrepds

-- This work by Nick Scheel is licensed under CC0 1.0
-- https://creativecommons.org/publicdomain/zero/1.0/

-- 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.