File tree Expand file tree Collapse file tree 5 files changed +7
-7
lines changed
Expand file tree Collapse file tree 5 files changed +7
-7
lines changed Original file line number Diff line number Diff line change 11# Attributes
22
3- Mathlib version: ` b514609d17aaa0e85b230131a8239f2d0e822af6 `
3+ Mathlib version: ` f741387cc3de9871a6bb1cb250947059176dbe20 `
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: ` b514609d17aaa0e85b230131a8239f2d0e822af6 `
3+ Mathlib version: ` f741387cc3de9871a6bb1cb250947059176dbe20 `
44
55## \# adaptation_note
66Defined in: ` adaptationNoteCmd `
Original file line number Diff line number Diff line change 11# Options
22
3- Mathlib version: ` b514609d17aaa0e85b230131a8239f2d0e822af6 `
3+ Mathlib version: ` f741387cc3de9871a6bb1cb250947059176dbe20 `
44
55## Elab.async
66type: ` Bool `
Original file line number Diff line number Diff line change 11# Tactics
22
3- Mathlib version: ` b514609d17aaa0e85b230131a8239f2d0e822af6 `
3+ Mathlib version: ` f741387cc3de9871a6bb1cb250947059176dbe20 `
44
55## \# adaptation_note
66Defined in: ` «tactic#adaptation_note_» `
@@ -1053,7 +1053,7 @@ Defined in: `Batteries.Tactic.byContra`
10531053introducing a hypothesis ` h : ¬p ` and proving ` False ` .
10541054* If ` p ` is a negation ` ¬q ` , ` h : q ` will be introduced instead of ` ¬¬q ` .
10551055* If ` p ` is decidable, it uses ` Decidable.byContradiction ` instead of ` Classical.byContradiction ` .
1056- * If ` h ` is omitted, the introduced variable ` _: ¬p ` will be anonymous .
1056+ * If ` h ` is omitted, the introduced variable will be called ` this ` .
10571057
10581058## by_contra!
10591059Defined in: ` byContra! `
Original file line number Diff line number Diff line change 55 "type" : " git" ,
66 "subDir" : null ,
77 "scope" : " " ,
8- "rev" : " b514609d17aaa0e85b230131a8239f2d0e822af6 " ,
8+ "rev" : " f741387cc3de9871a6bb1cb250947059176dbe20 " ,
99 "name" : " mathlib" ,
1010 "manifestFile" : " lake-manifest.json" ,
1111 "inputRev" : " master" ,
7575 "type" : " git" ,
7676 "subDir" : null ,
7777 "scope" : " leanprover-community" ,
78- "rev" : " 26884086fb66f99b56ed363c5e54bfcc70238599 " ,
78+ "rev" : " c0b0d08446817bd410548d9ea8ddcccf5d89f63f " ,
7979 "name" : " batteries" ,
8080 "manifestFile" : " lake-manifest.json" ,
8181 "inputRev" : " main" ,
You can’t perform that action at this time.
0 commit comments