diff options
| author | Andreas Grois <andi@grois.info> | 2024-01-25 23:58:30 +0100 |
|---|---|---|
| committer | Andreas Grois <andi@grois.info> | 2024-01-25 23:58:30 +0100 |
| commit | 5a5ef3bb65cc41537b44df9d43446232c83230d0 (patch) | |
| tree | d34604e78e0ccce8d74faca009d605204e5d59a1 /Common/Substring.lean | |
| parent | 212e250861f65fdddadbae1e8c79e4617ea36051 (diff) | |
Make Find function take a predicate. Simplify PopLast.
Diffstat (limited to 'Common/Substring.lean')
0 files changed, 0 insertions, 0 deletions