2 ms·
I can’t fathom anyone who has actually spent significant time performing mathematical manipulations with pencil and paper thinking that this is a good idea. Mat
by leephillips 4y ago
I can’t fathom anyone who has actually spent significant time performing mathematical manipulations with pencil and paper thinking that this is a good idea. Mathematicians have evolved notational conventions that work well for reading, writing, and calculation.
- jameshart 4y agoAnd I can't fathom why anyone would prefer to declare fundamental components of their proof using identifiers as terse as this: nominal_datatype fm = Mem tm tm (infixr "IN" 150) | Eq tm tm (infixr "EQ" 150) | Disj fm fm (infixr "OR" 130) | Neg fm | Ex x::name f::fm binds x in f These are not pencil-paper formula notation, they are declarations of named entities, and they don't need to. be so terse.
- ajb 4y agoThese are obvious abbreviations in the context. If you're working on a proof you might not want lots of 'theorem' and 'formula' to clutter up your screen. The programming world converged on full word variables, but it also converged on {} instead of BEGIN END etc. Alex