Should all propositions be wrapped in Proof?

matt-noonan / gdp

Ghosts of Departed Proofs

BSD 3-Clause "New" or "Revised" License

60 stars 11 forks source link

Should all propositions be wrapped in Proof? #8

Closed brnzhg closed 4 years ago

brnzhg commented 4 years ago

https://github.com/matt-noonan/gdp/blob/6e09928c2c2f5467e09dfc69310d6b67d6361422/src/Theory/Equality.hs#L87-L88

It seems like there was a change at some point to wrap all propositions in the Proof type, but apply and substitute require (x == x') rather than Proof (x == x'). Was this just overlooked or am I misunderstanding?

matt-noonan commented 4 years ago

@brnzhg Just overlooked, I think. Thanks for catching this!

matt-noonan commented 4 years ago

Resolved by #9