Commit 2021-10-18 09:49 6b8b2390

View on Github →

feat: ext tactic (#73)

ext : 42 is not implemented yet
@[ext] structure Foo is not supported by core (yet?), so I have implemented a cool workaround

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Prod.lean

modified theorem Prod.map_def

Modified Mathlib/Data/Subtype.lean

Modified Mathlib/Init/Logic.lean

Modified Mathlib/Logic/Basic.lean

modified theorem xor_false

modified theorem xor_true

Modified Mathlib/Logic/Function/Basic.lean

Modified Mathlib/Tactic/Basic.lean

Created Mathlib/Tactic/Ext.lean

added structure Mathlib.Tactic.Ext.$n:ident

added def Mathlib.Tactic.Ext.mkAndN

added def Mathlib.Tactic.Ext.mkIff

added def Mathlib.Tactic.Ext.withExtHyps

Modified Mathlib/Tactic/NormNum.lean

deleted def Lean.Tactic.evalNormNum

Created test/ext.lean

added structure A

added structure B

added structure C