guardHyp

Stream: mathlib4

[Moritz Doll]

Where did docs4#guardHyp go? Also the generated docs seem to be very out of date

[Johan Commelin]

Voila: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/choose/near/298770777

[Moritz Doll]

I've gotten a version of guardHyp for conv to work by mindless copy and paste (I am getting really good at that at least). In order that there is no duplicated code, I think that the original evalGuardHyp should be changed so that it calls another function that does the heavy lifting and evalGuardHyp just does the elaboration of the syntax. Does that sound about right?

I.e., change evalGuardHyp to something like this:

@[inheritDoc guardHyp, tactic guardHyp] def evalGuardHyp : Lean.Elab.Tactic.Tactic := fun
  | `(tactic| guard_hyp $h $[$c $ty]? $[$eq $val]?) => evalGuardHyp' h c ty eq val

then the new conv-tactic is just

@[inheritDoc guardHyp, tactic convGuardHyp] def evalConvGuardHyp : Lean.Elab.Tactic.Tactic := fun
  | `(conv| guard_hyp $h $[$c $ty]? $[$eq $val]?) => evalGuardHyp' h c ty eq val

[Mario Carneiro]

You should probably PR that to std along with the new tactic then

[Moritz Doll]

First PR is here std4#11
https://github.com/leanprover/std4/pull/11

[Moritz Doll]

zulip links std4 to https://github.com/leanprover-community/std4/ not https://github.com/leanprover/std4/

[Mario Carneiro]

std4#11 -- fixed

[Moritz Doll]

Thanks Mario, this looks so much better than what I came up with. for some reason I assumed that conv was implemented in Mathlib and I was going to make two PRs, but this is way better. Shouldn't dsimp then be in Lean4?

[Mario Carneiro]

dsimp is in lean 4

[Moritz Doll]

I meant dsimp for conv, this PR mathlib4#419

[Moritz Doll]

I doesn't really make sense in Mathlib4 if everything it needs is in Lean4 already

[Mario Carneiro]

Almost everything in std "could be in lean 4 already"

[Mario Carneiro]

but if it's not required for implementing lean itself then there is a general discouragement of new additions to the bootstrap

[Mario Carneiro]

However, it is true that many things that are currently going in mathlib4 should go in std4 eventually. Std has higher standards than mathlib4, and it is not as much focused on backward compatibility with mathlib so new tactics should be justified for being generally useful rather than being needed for the port