lean4-htt/src/Init/Data/Fin
2021-03-11 11:19:33 -08:00
..
Basic.lean chore: use new notation 2021-03-11 11:19:33 -08:00