Kyle Miller
Kyle Miller
Work in progress and tentative -- I'm not sure if this is implemented correctly.
This is a work in progress
### Prerequisites * [X] Put an X between the brackets on this line if you have done all of the following: * Checked that your issue isn't already [filed](https://github.com/leanprover-community/lean/issues). *...
Constructors for single-vertex and single-edge subgraphs along with some associated properties. Also includes dot notation improvements for `simple_graph.subgraph.adj`. Co-authored-by: Joanna Choules --- [](https://gitpod.io/from-referrer/)
Dot notation for functions does not behave in an expected way when there are type families. For example, if we define a dependent `Function.swap` function, we might expect (or at...
This PR makes two modifications to the pretty printer for pi types: (1) if `α` is a Type and `p` is a Prop then `α → p` pretty prints as...
Provides walks, trails, paths, cycles, forests, and trees. Walks are set up so that `G.walk v w` is the type of all walks between vertices `v` and `w`, and it...
This was suggested by Scott Morrison to be able to help projects adjust to `Nat` having built-in custom eliminators.
Implements a Lean 3 pretty printer feature. Structures with the `@[pp_using_anonymous_constructor_attribute]` pretty print like `⟨x, y, z⟩` rather than `{a := x, b := y, c := z}`. Adds this...
It's often confusing how `fun x y => ?foo` elaborates as `fun x y => ?m.123 x y`, with no way to see how `?m.123` is connected to `?foo`. This...