commit: 2e4557dbd0a0641a8ab6f9c660f9c96504b785b4

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

Wed Feb 28 01:53:25 2024 +1100
committer: GitHub <noreply@github.com>

Tue Feb 27 14:53:25 2024 +0000
tree: f82e1c3d4ae43d28c8cb3b0e9f6a70ef1d0705c7
parent: 7d5b6cf097c435a5e45e4549115945f4f577fc56 [diff]

chore: default for librarySearch tactic argument (#3495)

There's a downstream tactic in Mathlib that calls `librarySearch`, and
it's easier it is has a default provided.

2 files changed

tree: f82e1c3d4ae43d28c8cb3b0e9f6a70ef1d0705c7

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.