search

Soonad / Base.fm

Standard library for the Formality language
http://tiny.cc/8nvvgz
MIT License
18 stars 2 forks source link

Strange `nand` and `nor` #1

Closed semenov-vladyslav closed 5 years ago

semenov-vladyslav commented 5 years ago

nand and xor from Data.Bool are equal. nand x y is usually defined to be equal to and (not x) y.

nor x y is equal to not (or (not x) (not y)) which is a slightly unconventional definition of nor.

VictorTaelin commented 5 years ago

Thanks!

@johnchandlerburnham explain yourself!

johnchandlerburnham commented 5 years ago

Last I remember leaving Data.Bool is looking like this: https://gitlab.com/moonad/Formality-Base/blob/jcb/scratch/Bool.fm, with the binop abstraction and operators. OTOH, I make many careless mistakes, so if I did this I apologize!

Regardless, this implies two follow-up issues:

  1. We should have more identities in Data.Bool to catch errors like this. And we should think about how to scalably add proofs to other data structures to prevent errors like this in other files. Call it: "Proof-Driven Development"
  2. We should decide whether/how to add operator syntax back to Base given our recent refactors.

I will create new issues around #1 and #2 when I get back from my honeymoon