2 ms·

And I can't fathom why anyone would prefer to declare fundamental components of their proof using identifiers as terse as this: nominal_datatype fm =

And 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 ago
These 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