\(
\newcommand\D{\mathrm{d}}
\newcommand\E{\mathrm{e}}
\newcommand\I{\mathrm{i}}
\newcommand\bigOh{\mathcal{O}}
\newcommand{\cat}[1]{\mathbf{#1}}
\newcommand\curl{\vec{\nabla}\times}
\newcommand{\CC}{\mathbb{C}}
\newcommand{\NN}{\mathbb{N}}
\newcommand{\QQ}{\mathbb{Q}}
\newcommand{\RR}{\mathbb{R}}
\newcommand{\ZZ}{\mathbb{Z}}
\)
"Element of" - Mizar
It's possible to write things like let x be Element of {} in
Mizar. This isn't a typing error, arguably, since {} is a term whose
type is set. I believe later on, in the CHECKER, it's treated as it
(logically) should.
Last Updated 2022-05-25 Wed 11:20.