Idris2/tests/idris2/reg021/case.idr

twice : Char -> Char -> Char -> Char -> Nat -> (Nat, Nat)
twice w x y z Z = (Z, Z)
twice m n o p (S x)
    = case twice m n o p x of
           (a, b) => (S a, S b)

bothS : Int -> String -> (Nat, Nat) -> (Nat, Nat)
bothS test dummy = \(c, d) => (S c, S d)

pf : (x : Nat) -> twice 'a' 'b' 'c' 'd' (S x) 
                     = bothS 99 "red balloons" (twice 'a' 'b' 'c' 'd' x)
pf k = Refl -- Refl
Look inside case blocks in conversion check This is quite fiddly as it the blocks might be in different contexts so we need to keep track of which variables correspond in the scrutinees of the blocks. Once that's done, check the terms at the leaves convert, then check the corresponding variables convert. This may not be perfect yet, because we only look at case scrutinees to find correspondence. It might also be a bit slower than it could be, but at least these checks are quite rare. Fixes #208 and maybe some others? 2020-06-04 20:21:44 +03:00			`twice : Char -> Char -> Char -> Char -> Nat -> (Nat, Nat)`
			`twice w x y z Z = (Z, Z)`
			`twice m n o p (S x)`
			`= case twice m n o p x of`
			`(a, b) => (S a, S b)`

			`bothS : Int -> String -> (Nat, Nat) -> (Nat, Nat)`
			`bothS test dummy = \(c, d) => (S c, S d)`

			`pf : (x : Nat) -> twice 'a' 'b' 'c' 'd' (S x)`
			`= bothS 99 "red balloons" (twice 'a' 'b' 'c' 'd' x)`
			`pf k = Refl -- Refl`