test: add structure field default value test

This commit is contained in:
Leonardo de Moura 2020-12-23 08:35:27 -08:00
parent f53721e1c9
commit 74686a149a
2 changed files with 17 additions and 0 deletions

View file

@ -0,0 +1,11 @@
structure A where
f : Nat → Nat → Nat
structure B extends A where
f (a b : Nat) := 10
structure C extends A where
f a b := 0
structure D extends A where
f a b := true -- error

View file

@ -0,0 +1,6 @@
structDefault.lean:11:11: error: type mismatch
true
has type
Bool
but is expected to have type
Nat