Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-04-05 14:37 78a08ebc

View on Github →

feat(data/mllist): monadic lazy lists (#865)

  • feat(data/mllist): monadic lazy lists
  • oops, fix header
  • shove into tactic namespace
  • make mllist into a monad (#880)
  • make mllist into a monad
  • looks good. add take, and some tests
  • update authors
  • cleanup test

Estimated changes

added def F
added def S
added def append