Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
chore: empty ports of the Data/Buffer/Parser files (#5848)
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
- Loading branch information
1 parent
98ab6ea
commit b41e763
Showing
4 changed files
with
48 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,15 @@ | ||
/- | ||
Copyright (c) 2020 Yakov Pechersky. All rights reserved. | ||
Released under Apache 2.0 license as described in the file LICENSE. | ||
Authors: Yakov Pechersky | ||
! This file was ported from Lean 3 source module data.buffer.basic | ||
! leanprover-community/mathlib commit 2220b0cbab795e73674b8191170b0cc68c6b54a8 | ||
! Please do not edit these lines, except to modify the commit id | ||
! if you have ported upstream changes. | ||
Porting note: | ||
As the parsing framework has completely changed in Lean 4 | ||
there is no point porting these files directly. | ||
They can be rewritten from scratch as needed, just as for tactics. | ||
-/ |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,15 @@ | ||
/- | ||
Copyright (c) 2020 Yakov Pechersky. All rights reserved. | ||
Released under Apache 2.0 license as described in the file LICENSE. | ||
Authors: Yakov Pechersky | ||
! This file was ported from Lean 3 source module data.buffer.parser.basic | ||
! leanprover-community/mathlib commit 2220b0cbab795e73674b8191170b0cc68c6b54a8 | ||
! Please do not edit these lines, except to modify the commit id | ||
! if you have ported upstream changes. | ||
Porting note: | ||
As the parsing framework has completely changed in Lean 4 | ||
there is no point porting these files directly. | ||
They can be rewritten from scratch as needed, just as for tactics. | ||
-/ |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,15 @@ | ||
/- | ||
Copyright (c) 2020 Yakov Pechersky. All rights reserved. | ||
Released under Apache 2.0 license as described in the file LICENSE. | ||
Authors: Yakov Pechersky | ||
! This file was ported from Lean 3 source module data.buffer.parser.numeral | ||
! leanprover-community/mathlib commit 2220b0cbab795e73674b8191170b0cc68c6b54a8 | ||
! Please do not edit these lines, except to modify the commit id | ||
! if you have ported upstream changes. | ||
Porting note: | ||
As the parsing framework has completely changed in Lean 4 | ||
there is no point porting these files directly. | ||
They can be rewritten from scratch as needed, just as for tactics. | ||
-/ |