Commit 2022-02-21 14:49 55441938

feat: (↑) notation for coercions (#199) See https://github.com/leanprover-community/mathport/issues/116#issuecomment-1046836990 The notation is a bit problematic for the pretty-printer, as it doesn't automatically insert parentheses to disambiguate it from the built-in coercion notation. Alternatives:

1. Use a different token.
2. Magically define (↑ ∙) to be the eta-reduction of fun x => ↑x. PS: the old macro for ↑ x was redundant since it's been moved to core some time ago.