Idris2-boot/tests/chez/chez006/expected

"Nat"
"List of Nat"
"List of Something else"
"List of Something else"
"List of Bool"
"Int"
"Something else"
"List of Type"
"List of Int"
43
42
1/1: Building TypeCase (TypeCase.idr)
Main> Main> Main.strangeId is total
Main> Main.strangeId':
strangeId' _
Main> Bye for now!
1/1: Building TypeCase2 (TypeCase2.idr)
TypeCase2.idr:5:14--5:17:While processing left hand side of Main.strangeId at TypeCase2.idr:5:1--6:1:
Can't match on Nat (Erased argument)
TypeCase2.idr:9:5--9:9:While processing left hand side of Main.foo at TypeCase2.idr:9:1--10:1:
Can't match on Nat (Erased argument)
Updating typecase, add tests 2019-06-29 23:32:19 +03:00			`"Nat"`
			`"List of Nat"`
			`"List of Something else"`
			`"List of Something else"`
			`"List of Bool"`
			`"Int"`
			`"Something else"`
			`"List of Type"`
			`"List of Int"`
			`43`
			`42`
			`1/1: Building TypeCase (TypeCase.idr)`
			`Main> Main> Main.strangeId is total`
			`Main> Main.strangeId':`
			`strangeId' _`
			`Main> Bye for now!`
			`1/1: Building TypeCase2 (TypeCase2.idr)`
Better approach to erasure in pattern matching It's a big patch, but the summary is that it's okay to use a pattern in an erased position if either: - the pattern can also be solved by unification (this is the same as 'dot patterns' for matching on non-constructor forms) - the argument position is detaggable w.r.t. non-erased arguments, which means we can tell which pattern it is without pattern matching The second case, in particular, means we can still pattern match on proof terms which turn out to be irrelevant, especially Refl. Fixes #178 2020-01-21 21:47:43 +03:00			`TypeCase2.idr:5:14--5:17:While processing left hand side of Main.strangeId at TypeCase2.idr:5:1--6:1:`
			`Can't match on Nat (Erased argument)`
			`TypeCase2.idr:9:5--9:9:While processing left hand side of Main.foo at TypeCase2.idr:9:1--10:1:`
			`Can't match on Nat (Erased argument)`