Mathlib v3 is deprecated. Go to Mathlib v4

Theorem alist.recursion_insert_mk

Modification history

2023-01-20 00:18

src/data/list/alist.lean

feat(data/list/alist): recursion on `alist` using `insert` (#15434)

Added alist.recursion_insert_mk View on Github →