Mathlib v3 is deprecated. Go to Mathlib v4

Theorem primrec.subtype_mk

Modification history

2020-05-07 22:43
src/computability/primrec.lean
feat(data/equiv/encodable): `ulower` lowers countable types to `Type 0` (#2574) …
Added primrec.subtype_mkView on Github →