Mathlib v3 is deprecated. Go to Mathlib v4

Def holor_index

Modification history

2022-06-08 09:31

src/data/holor.lean

golf(*): `λ _, default` → `default` (#14608)

Modified holor_index View on Github →

2018-10-01 18:10

data/holor.lean

cleanup(data/holor)

Modified holor_index View on Github →

2018-10-01 14:51

data/holor.lean

feat(data/holor): holor library

Added holor_index View on Github →