Commit 2021-11-08 09:32 b0c3952f

refactor(Mathport): move mathport prelude to mathlib4 (#80) Moving Mathport/Prelude/* out of mathport into mathlib4. I've added a README that will hopefully help bystanders:

Mathport prelude
===
This directory contains instructions for `mathport`,
helping it to translate `mathlib` and align declarations and tactics with `mathlib4`.
(These files were formerly part of `mathport`, in the directory `Mathport/Prelude/`.)
`SpecialNames.lean`
: Contains `#align X Y` statements, where `X` is an identifier from mathlib3
  which should be aligned with the identifier `Y` from mathlib4.
  Sometimes we need `#align` statements just to handle exceptions to casing rules,
  but there are also many exceptional cases.
`Syntax.lean`
: Contains unimplemented stubs of tactics which need to be migrated from Lean3 to Lean4.
  When porting tactics, you can move the relevant stubs to a new file and
  use them as a starting point.
  Please make sure this file stays in sync with new tactic implementations
  (and in particular that the syntax is not defined twice).
  Please preserve the syntax of existing mathlib tactics,
  so that there are no unnecessary parse errors in the source files generated by `synport`.
  It is fine to fail with an error message for unimplemented features for now.