commit: 831fa0899fd0397e5a8f21abc2c5fcee8883c481

[log]
author: Kim Morrison <scott.morrison@gmail.com>

Wed Oct 16 13:41:17 2024 +1100
committer: GitHub <noreply@github.com>

Wed Oct 16 02:41:17 2024 +0000
tree: 785628f8b6de9b31c4ceb7c331b8420d251c2f9a
parent: 94053c9b1b79332a825c3a43d593bb0bdffb0956 [diff]

chore: upstream String.dropPrefix? (#5728)

Useful String helper functions widely used in tactic implementations.

src/Init/Data/String/Basic.lean[diff]

1 file changed

tree: 785628f8b6de9b31c4ceb7c331b8420d251c2f9a

README.md

This is the repository for Lean 4.

About

Installation

See Setting Up Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean (documentation source: doc/make/index.md).