max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

test: specialize attribute tests

Browse source
This commit is contained in:
Leonardo de Moura 2022-09-07 16:32:25 -07:00
parent 19f5fe6f42
commit 5c00708b7f
2 changed files with 29 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
tests/lean/specializeAttr.lean Normal file
View file

@ -0,0 +1,23 @@
@[specialize f g h]
def f1 (f : Nat → Nat) (g : Nat → Nat) (x : Nat) :=
f (f (g x))
@[specialize f 1 g]
def f2 (f : Nat → Nat) (g : Nat → Nat) (x : Nat) :=
f (f (g x))
@[specialize 1 f g]
def f3 (f : Nat → Nat) (g : Nat → Nat) (x : Nat) :=
f (f (g x))
@[specialize 0 g]
def f4 (f : Nat → Nat) (g : Nat → Nat) (x : Nat) :=
f (f (g x))
@[specialize 10]
def f5 (f : Nat → Nat) (g : Nat → Nat) (x : Nat) :=
f (f (g x))
@[specialize ff]
def f6 (f : Nat → Nat) (g : Nat → Nat) (x : Nat) :=
f (f (g x))

6
tests/lean/specializeAttr.lean.expected.out Normal file
View file

@ -0,0 +1,6 @@
specializeAttr.lean:1:17-1:18: error: invalid specialization argument name `h`, `f1` does have an argument with this name
specializeAttr.lean:5:15-5:16: error: invalid specialization argument index, `f` has already been specified as a specialization candidate
specializeAttr.lean:9:15-9:16: error: invalid specialization argument name `f`, it has already been specified as a specialization candidate
specializeAttr.lean:13:13-13:14: error: invalid specialization argument index, index must be greater than 0
specializeAttr.lean:17:13-17:15: error: invalid argument index, `f5` has #3 arguments
specializeAttr.lean:21:13-21:15: error: invalid specialization argument name `ff`, `f6` does have an argument with this name