mathlib
ea10944c - feat(data/list/defs): list.singleton_append and list.bind_singleton (#3298)

Commit
5 years ago
feat(data/list/defs): list.singleton_append and list.bind_singleton (#3298) I found these useful when working with palindromes and Fibonacci words respectively. While `bind_singleton` is available as a monad law, I find the specialized version more convenient.
Author
Parents
Loading