7 lines
145 B
Text
7 lines
145 B
Text
inductive Bar
|
|
| foobar : Foo → Bar
|
|
| somelist : List Bar → Bar
|
|
|
|
inductive Bar2
|
|
| foobar : (x : Foo) → Bar2
|
|
| somelist : List Bar2 → Bar2
|