Idris2/tests/idris2/data/record001/expected

1/1: Building Record (Record.idr)
Main> [1, 2, 3, 4, 5]
Main> [1, 2, 3, 4, 5]
Main> some_fn testPerson : Nat -> Nat
Main> Bye for now!
Add test script They don't all pass yet, for minor reasons. Coming shortly... Unfortunately the startup overhead for chez is really noticeable here! 2020-05-19 20:25:18 +03:00			`1/1: Building Record (Record.idr)`
			`Main> [1, 2, 3, 4, 5]`
			`Main> [1, 2, 3, 4, 5]`
Fix performance regression #1991 (#1995) * Normalise types fully at the REPL It was a bit odd that we only normalised the scope of function types and not the arguments, and I can't remember the reason for that if there even was one. * Better way of using nf_metavars_threshold If a term is getting big and probably needs normalising, we now have a sizeLimit flag in quote, so we can use that instead of checking the size afterwards. This is a handy heuristic for speeding up unification when there's a term with lots of suspended computation. Fixes #1991 2021-10-12 01:53:52 +03:00			`Main> some_fn testPerson : Nat -> Nat`
Add test script They don't all pass yet, for minor reasons. Coming shortly... Unfortunately the startup overhead for chez is really noticeable here! 2020-05-19 20:25:18 +03:00			`Main> Bye for now!`