File tree Expand file tree Collapse file tree 5 files changed +33
-5
lines changed
Expand file tree Collapse file tree 5 files changed +33
-5
lines changed Original file line number Diff line number Diff line change 11# Attributes
22
3- Mathlib version: ` 337f3a7ec82d927c2939d3e695573f43e5aa0874 `
3+ Mathlib version: ` aa78411076513560baa4507bc5edb5bccbf51741 `
44
55## Std.Internal.tree_tac
66 simp theorems used by internal DTreeMap lemmas
Original file line number Diff line number Diff line change 11# Commands
22
3- Mathlib version: ` 337f3a7ec82d927c2939d3e695573f43e5aa0874 `
3+ Mathlib version: ` aa78411076513560baa4507bc5edb5bccbf51741 `
44
55## \# adaptation_note
66Defined in: ` adaptationNoteCmd `
Original file line number Diff line number Diff line change 11# Options
22
3- Mathlib version: ` 337f3a7ec82d927c2939d3e695573f43e5aa0874 `
3+ Mathlib version: ` aa78411076513560baa4507bc5edb5bccbf51741 `
44
55## Elab.async
66type: ` Bool `
@@ -1145,6 +1145,34 @@ default: `false`
11451145
11461146
11471147
1148+ ## linter.tacticAnalysis.tryAtEachStepAesop
1149+ type: ` Bool `
1150+
1151+ default: ` false `
1152+
1153+
1154+
1155+ ## linter.tacticAnalysis.tryAtEachStepGrind
1156+ type: ` Bool `
1157+
1158+ default: ` false `
1159+
1160+
1161+
1162+ ## linter.tacticAnalysis.tryAtEachStepGrindPremises
1163+ type: ` Bool `
1164+
1165+ default: ` false `
1166+
1167+
1168+
1169+ ## linter.tacticAnalysis.tryAtEachStepSimpAll
1170+ type: ` Bool `
1171+
1172+ default: ` false `
1173+
1174+
1175+
11481176## linter.toAdditiveExisting
11491177type: ` Bool `
11501178
Original file line number Diff line number Diff line change 11# Tactics
22
3- Mathlib version: ` 337f3a7ec82d927c2939d3e695573f43e5aa0874 `
3+ Mathlib version: ` aa78411076513560baa4507bc5edb5bccbf51741 `
44
55## \# adaptation_note
66Defined in: ` «tactic#adaptation_note_» `
Original file line number Diff line number Diff line change 55 "type" : " git" ,
66 "subDir" : null ,
77 "scope" : " " ,
8- "rev" : " 337f3a7ec82d927c2939d3e695573f43e5aa0874 " ,
8+ "rev" : " aa78411076513560baa4507bc5edb5bccbf51741 " ,
99 "name" : " mathlib" ,
1010 "manifestFile" : " lake-manifest.json" ,
1111 "inputRev" : " master" ,
You can’t perform that action at this time.
0 commit comments