miscelleaneous

Random Lean experiments

Lean automatically inserts else pure ()

Changes

1 changed files (+1/-3)