mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-12-26 14:21:52 +03:00
86eb475413
We were only checking parameters, meaning that there were potential clashes leading to confusing behaviour, and meaning that it was somehow relevant what the names were in the interface!
13 lines
252 B
Plaintext
13 lines
252 B
Plaintext
1/1: Building Odd (Odd.idr)
|
|
Welcome to Idris 2 version 0.0. Enjoy yourself!
|
|
Main> 0 v : Type
|
|
0 k' : Type
|
|
0 k : Type
|
|
conArg : Eq k
|
|
z : List (k', v)
|
|
y : v
|
|
x : k'
|
|
-------------------------------------
|
|
bang : List (k', v)
|
|
Main> Bye for now!
|