Dead code in proof tree #3

New Issue

aniva · 2023-08-22T20:26:43-07:00

aniva commented

2023-08-22 20:26:43 -07:00

The name field seems to be unnecessary after TermElabM became the outermost monad used in the proof tree system:

structure ProofStart where
  name: Option String     -- Identifier of the proof
  ...

structure ProofTree where
  -- All parameters needed to run a `TermElabM` monad
  name: Name
  ...

This field has no usage in Tactic.lean so it should be removed

The `name` field seems to be unnecessary after `TermElabM` became the outermost monad used in the proof tree system: ```lean4 structure ProofStart where name: Option String -- Identifier of the proof ... structure ProofTree where -- All parameters needed to run a `TermElabM` monad name: Name ... ``` This field has no usage in `Tactic.lean` so it should be removed

aniva added this to the 0.2.6 milestone 2023-08-22 20:26:43 -07:00

aniva added the

category

optimization

part/Goal

labels 2023-08-22 20:26:43 -07:00

aniva self-assigned this 2023-08-22 20:26:43 -07:00

aniva added reference misc/cleanup

2023-08-23 13:15:27 -07:00

aniva referenced this issue

2023-08-23 13:21:36 -07:00

Remove dead code and consolidate error types #5