mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-25 20:51:43 +03:00
ff7d3a0246
That is, don't generalise multiplicities, because we need the hole type to be precise wrt multiplicities. Resolves #189
21 lines
618 B
Plaintext
21 lines
618 B
Plaintext
1/1: Building linholes (linholes.idr)
|
|
Main> 0 c : Type
|
|
0 b : Type
|
|
0 a : Type
|
|
f : ((1 _ : a) -> (1 _ : b) -> (1 _ : c) -> ()) -> ()
|
|
-------------------------------------
|
|
foo1h : (1 _ : a) -> (1 _ : b) -> (1 _ : c) -> ()
|
|
Main> 0 c : Type
|
|
0 b : Type
|
|
0 a : Type
|
|
f : ((1 _ : a) -> (1 _ : b) -> (1 _ : c) -> ()) -> ()
|
|
-------------------------------------
|
|
foo2h : (1 _ : a) -> (1 _ : b) -> (1 _ : c) -> ()
|
|
Main> 0 c : Type
|
|
0 b : Type
|
|
0 a : Type
|
|
f : ((1 _ : a) -> (1 _ : b) -> (1 _ : c) -> ()) -> ()
|
|
-------------------------------------
|
|
foo3h : (1 _ : a) -> (1 _ : b) -> (1 _ : c) -> ()
|
|
Main> Bye for now!
|