lean4-htt/src/Init/Data/String
2021-07-19 09:55:37 +02:00
..
Basic.lean chore: expose Substring.prev/next 2021-07-19 09:55:37 +02:00
Extra.lean chore: remove #lang lean4 header 2020-10-25 09:54:07 -07:00