Tag: decidability

Decidable propositions III

We’ve seen the basics of decidable in Decidable propositions I and if-then-else constructions in Decidable propostions II. Now, we’ll see how to prove results through type class inference. If you’ve been following along and recreating decidable in your own hidden namespace, it’s now time to declare an important, albeit trivial, instance. That is, it is […]

Decidable propositions II

Recall from our previous post the definition of decidable. We’ll later discuss how this class works in conjunction with type class inference to automate proofs of decidable propositions. In this post, we show how conditionals are implemented in Lean using the decidable recursor. If-then-else The ite function is one of two Lean implementations of an […]