Idris2-boot/tests/ttimp/eta001/expected

Processing as TTImp
Written TTC
Yaffle> ((Main.Refl [Just {b:10} = Main.Nat]) [Just x = (Main.S (Main.S (Main.S (Main.S Main.Z))))])
Yaffle> Main.etaGood1 : ((((Main.Eq [Just b = (%pi RigW Explicit Nothing Integer (%pi RigW Explicit Nothing Integer Main.Test))]) [Just a = (%pi RigW Explicit Nothing Integer (%pi RigW Explicit Nothing Integer Main.Test))]) Main.MkTest) (%lam RigW Explicit Just x Integer (%lam RigW Explicit Just y Integer ((Main.MkTest x) y))))
Yaffle> Bye for now!
Support eta in unification Also added (necessarily) a rule for lambdas 2019-05-07 17:06:00 +03:00			`Processing as TTImp`
			`Written TTC`
Implement occurs check properly (finally!) Instead of the previous unreliable hack, actually look for occurrences of the solved metavariable. Block if there are any, and fail if there are any under a constructor. I had expected this to hurt performance quite a bit, but it seems it doesn't. This was prompted by #304, which is now partly fixed, but there's still a refinement to unification needed to fix it fully (and at least it doesn't segfault due to the cycle now!) 2020-04-27 13:21:50 +03:00			`Yaffle> ((Main.Refl [Just {b:10} = Main.Nat]) [Just x = (Main.S (Main.S (Main.S (Main.S Main.Z))))])`
First attempt at linearity checking pass This slows things down a bit because to find the holes and give them the right multiplicities, we need to normalise all the arguments which might have been metavariables. Maybe we should skip this if we're not using anything linear, for efficiency? As patterns are handled by deciding which side of the as is considered 'used'. In case blocks, that should be the variable name, but in general it should be the pattern, so IAs now has a flag to say which one. 2019-05-19 22:24:14 +03:00			`Yaffle> Main.etaGood1 : ((((Main.Eq [Just b = (%pi RigW Explicit Nothing Integer (%pi RigW Explicit Nothing Integer Main.Test))]) [Just a = (%pi RigW Explicit Nothing Integer (%pi RigW Explicit Nothing Integer Main.Test))]) Main.MkTest) (%lam RigW Explicit Just x Integer (%lam RigW Explicit Just y Integer ((Main.MkTest x) y))))`
Support eta in unification Also added (necessarily) a rule for lambdas 2019-05-07 17:06:00 +03:00			`Yaffle> Bye for now!`