CODEWITHSUNDEEP
idristypecheckingformal-verification
ggg
ggg

Reputation: 21

Constructed (0 = 1) in Idris 1.3.3?

While experimenting using Idris 1.3.3, I found that the following code file typechecks:

doubleCong: {f: Nat -> Nat -> Nat} -> (prf1: (a1 = a2)) -> (prf2: (b1 = b3)) -> (f a1 b1 = f a2 b2)
doubleCong {f} prf1 prf2 = let intermediate = cong {f = f} prf1 in case intermediate of
                                                                        Refl impossible

zero_equals_1: (Z = S Z)
zero_equals_1 = doubleCong {b2=1} {f = (+)} (Refl {x=0}) (Refl {x=0})


anything: (a: Type) -> a
anything a = case zero_equals_1 of
                  Refl impossible

Evaluating in repl:

Evaluating in repl

Shouldn't it be impossible to construct a value of type (Z = S Z)?

Note: it doesn't typecheck in Idris 2 version 0.3.0, only Idris 1.3.3

Upvotes: 0

Views: 16

Answers (0)

Related Questions