mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-17 16:21:46 +03:00
2a75731916
So the type of Elab now gives the expected type that's being elaborated to, meaning that we can run 'check' in the middle of scripts and use the result.
6 lines
129 B
Plaintext
6 lines
129 B
Plaintext
1/1: Building power (power.idr)
|
|
Main> Main.cube : Nat -> Nat
|
|
cube = \x => mult x (mult x (mult x 1))
|
|
Main> 27
|
|
Main> Bye for now!
|