Re:My favorite Rust function
by foopdoopfoop on Saturday October 12, 2019 @07:42PM
(#21237141)
Reminds me of Coq's definition of `False`:
`Inductive False := .`
i.e., `False` has no constructors and hence is an empty type.
Anyway, this means that for any type `A`, you can construct a function of type `False -> A` because you just do this:
`fun (x : False) => match x with end.`
Since `False` has no constructors, a match statement on a value of type `False` has no cases to match on, and you're done. (Coq's type system requires a case for each constructor of the type of the thing being matched on.) This is why, if you assume something that is false, you can prove anything. :)
`Inductive False := .`
i.e., `False` has no constructors and hence is an empty type.
Anyway, this means that for any type `A`, you can construct a function of type `False -> A` because you just do this:
`fun (x : False) => match x with end.`
Since `False` has no constructors, a match statement on a value of type `False` has no cases to match on, and you're done. (Coq's type system requires a case for each constructor of the type of the thing being matched on.) This is why, if you assume something that is false, you can prove anything. :)