search

Smaug123 / agdaproofs

Mathematical proofs in Agda
MIT License
4 stars 1 forks source link

Remove axiom K from the definition of the integers #38

Closed Smaug123 closed 5 years ago

Smaug123 commented 5 years ago

Currently, for annoying reasons related to the definition of _<N_, we need axiom K to define the integers. Stop doing this!