max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: import orphaned Lean.Replay (#5693)

Browse source 
As noticed on
[zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.E2.9C.94.20Reverse.20FFI.20undefined.20reference.20for.20mathlib/near/475824204).
This commit is contained in:
Kim Morrison 2024-10-14 12:29:03 +11:00 • committed by GitHub
parent 7fd2aa04ae
commit 225e08965d
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/Lean.lean
View file

@ -37,3 +37,4 @@ import Lean.Linter
import Lean.SubExpr
import Lean.LabelAttribute
import Lean.AddDecl
import Lean.Replay