Idris2/tests/idris2/reflection002/expected

1/1: Building power (power.idr)
Main> Main.cube : Nat -> Nat
cube = \x => mult x (mult x (mult x 1))
Main> 27
Main> Main.cube' : Nat -> Nat
cube' = \x => mult (mult (plus x 0) x) x
Main> 27
Main> Bye for now!
Progress on elaborator reflection Add %runElab and start on scripts, although all they can do so far is check a term. This does gives us, sort of, "template Idris" (as demonstrated in test reflection002) 2020-05-31 03:36:54 +03:00			`1/1: Building power (power.idr)`
			`Main> Main.cube : Nat -> Nat`
In reflection, check now takes a concrete type 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. 2020-06-03 00:41:37 +03:00			`cube = \x => mult x (mult x (mult x 1))`
Progress on elaborator reflection Add %runElab and start on scripts, although all they can do so far is check a term. This does gives us, sort of, "template Idris" (as demonstrated in test reflection002) 2020-05-31 03:36:54 +03:00			`Main> 27`
Add alternative example to reflection002 A bit more typesafe... 2020-06-03 01:56:30 +03:00			`Main> Main.cube' : Nat -> Nat`
			`cube' = \x => mult (mult (plus x 0) x) x`
			`Main> 27`
Progress on elaborator reflection Add %runElab and start on scripts, although all they can do so far is check a term. This does gives us, sort of, "template Idris" (as demonstrated in test reflection002) 2020-05-31 03:36:54 +03:00			`Main> Bye for now!`