mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-29 22:51:51 +03:00
3120fcb84a
This is mostly to make it easier to write linear function types without having to invent names for everything, which might be noisy. Also it improves the display of linear function types when the name isn't used in the scope.
9 lines
763 B
Plaintext
9 lines
763 B
Plaintext
Processing as TTImp
|
|
Written TTC
|
|
Yaffle> Main.foo : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just {k:26} Main.Nat (%pi RigW Explicit Nothing a (%pi RigW Explicit Nothing ((Main.Vect {k:26}) a) (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just _ Main.Nat ((Main.Vect ((Main.plus {k:26}) m)) a))))))))
|
|
Yaffle> Bye for now!
|
|
Processing as TTC
|
|
Read TTC
|
|
Yaffle> Main.foo : (%pi Rig0 Explicit Just m Main.Nat (%pi Rig0 Explicit Just a %type (%pi Rig0 Explicit Just {k:26} Main.Nat (%pi RigW Explicit Nothing a (%pi RigW Explicit Nothing ((Main.Vect {k:26}) a) (%pi RigW Explicit Nothing ((Main.Vect m) a) (%pi Rig0 Explicit Just _ Main.Nat ((Main.Vect ((Main.plus {k:26}) m)) a))))))))
|
|
Yaffle> Bye for now!
|