File tree Expand file tree Collapse file tree 5 files changed +26
-5
lines changed
Expand file tree Collapse file tree 5 files changed +26
-5
lines changed Original file line number Diff line number Diff line change 11# Attributes
22
3- Mathlib version: ` 64ce1d71956f0be5bcd226237840f45de0f4e640 `
3+ Mathlib version: ` 5592362428bc73f430e2715b8fc3762686b86363 `
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: ` 64ce1d71956f0be5bcd226237840f45de0f4e640 `
3+ Mathlib version: ` 5592362428bc73f430e2715b8fc3762686b86363 `
44
55## \# adaptation_note
66Defined in: ` adaptationNoteCmd `
Original file line number Diff line number Diff line change 11# Options
22
3- Mathlib version: ` 64ce1d71956f0be5bcd226237840f45de0f4e640 `
3+ Mathlib version: ` 5592362428bc73f430e2715b8fc3762686b86363 `
44
55## Elab.async
66type: ` Bool `
@@ -2473,6 +2473,27 @@ default: `false`
24732473
24742474enable/disable tracing for the given module and submodules
24752475
2476+ ## trace.Elab.DiffGeo
2477+ type: ` Bool `
2478+
2479+ default: ` false `
2480+
2481+ enable/disable tracing for the given module and submodules
2482+
2483+ ## trace.Elab.DiffGeo.MDiff
2484+ type: ` Bool `
2485+
2486+ default: ` false `
2487+
2488+ enable/disable tracing for the given module and submodules
2489+
2490+ ## trace.Elab.DiffGeo.TotalSpaceMk
2491+ type: ` Bool `
2492+
2493+ default: ` false `
2494+
2495+ enable/disable tracing for the given module and submodules
2496+
24762497## trace.Elab.ProxyType
24772498type: ` Bool `
24782499
Original file line number Diff line number Diff line change 11# Tactics
22
3- Mathlib version: ` 64ce1d71956f0be5bcd226237840f45de0f4e640 `
3+ Mathlib version: ` 5592362428bc73f430e2715b8fc3762686b86363 `
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" : " 64ce1d71956f0be5bcd226237840f45de0f4e640 " ,
8+ "rev" : " 5592362428bc73f430e2715b8fc3762686b86363 " ,
99 "name" : " mathlib" ,
1010 "manifestFile" : " lake-manifest.json" ,
1111 "inputRev" : " master" ,
You can’t perform that action at this time.
0 commit comments