Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-08-31 01:45 2946088e

View on Github →

feat(tactic/explode): line by line proof display for proof terms

Estimated changes

Modified tactic/basic.lean

Created tactic/explode.lean

added def tactic.explode.head'

added inductive tactic.explode.status