Skip to content

Commit

Permalink
chore: cleanup for mathport update (#620)
Browse files Browse the repository at this point in the history
* `add_decl_doc` already exists in core (this declaration was just shadowing it)
* `setup_tactic_parser` is not planned for porting; the nearest equivalent is nothing at all
* `mk_simp_attribute` can mostly be aligned to `register_simp_attr`, and the remaining part (the `:= ids,*`) can't be supported at all and will give a suitable port message in mathport
* `std_next` alignment consistently gives a stack overflow when porting on my machine; I think this is a recent regression (possibly leanprover-community/mathport#192?) but this is a quick fix since this function doesn't matter too much.
  • Loading branch information
digama0 committed Nov 17, 2022
1 parent 3d0ca44 commit bf8af5f
Showing 2 changed files with 5 additions and 5 deletions.
5 changes: 5 additions & 0 deletions Mathlib/Init/Align.lean
Original file line number Diff line number Diff line change
@@ -157,6 +157,11 @@ actual theorems in the files.

/-! ## `init.data.quot` -/

/-! ## `init.data.random` -/

#align std_next stdNextₓ -- this should be defeq but verification causes a stack overflow
#align std_split stdSplitₓ

/-! ## `init.data.repr` -/

#align has_repr Repr
5 changes: 0 additions & 5 deletions Mathlib/Mathport/Syntax.lean
Original file line number Diff line number Diff line change
@@ -486,11 +486,6 @@ end Attr
namespace Command

/- N -/ syntax (name := addTacticDoc) (docComment)? "add_tactic_doc " term : command
/- N -/ syntax (name := addDeclDoc) docComment "add_decl_doc " ident : command

/- S -/ syntax (name := setupTacticParser) "setup_tactic_parser" : command
/- N -/ syntax (name := mkSimpAttribute) "mk_simp_attribute " ident
(" from" (ppSpace ident)+)? (" := " str)? : command

/- M -/ syntax (name := addHintTactic) "add_hint_tactic " tactic : command

0 comments on commit bf8af5f

Please sign in to comment.