batteries icon indicating copy to clipboard operation
batteries copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat: add function for refl and apply

Open mcdoll opened this issue 1 year ago • 2 comments

mcdoll avatar May 24 '23 07:05 mcdoll

Heartbeat check: is this PR still active? If it is then just give a thumbs up and I will delete this comment.

fgdorais avatar Jul 22 '24 21:07 fgdorais

The apply function is in core now as Lean.MVarId.applyConst, but I don't think refl? exists in core.

kmill avatar Jul 22 '24 21:07 kmill