04227701d6
@kha I found the real issue with these two tests. You have modified the compiler to ignore definitions containing `sorry` :)
9 lines
146 B
Text
9 lines
146 B
Text
structure S :=
|
|
(a : nat) (h : a > 0) (b : nat)
|
|
|
|
def f (s : S) :=
|
|
s.b - s.a
|
|
|
|
constant magic {p : Prop} : p
|
|
|
|
#eval f {a := 5, b := 30, h := magic }
|