e68e448070
It is better for TC resolution since the parameter can be inferred by typing constraints, and it addresses issue #1373
4 lines
86 B
Text
4 lines
86 B
Text
class Foo (d: Nat)
|
|
|
|
inductive Bar [i: ∀ d', d ≤ d' → Foo d']
|
|
| mk: Bar (i:=i)
|