Proof has phantom role - Githubissues

matt-noonan / gdp

Ghosts of Departed Proofs

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

60 stars 11 forks source link

Open Lysxia opened 1 year ago

Lysxia commented 1 year ago

bad :: Proof p -> Proof q
bad = coerce

contra :: Proof FALSE
contra = coerce true