MarcelineVQ · March 19, 2020 03:19
diff --git a/gistfile1.txt b/gistfile1.txt
 Feb 12 04:14:47 <MarcelineVQ>	gallais: is there a C-c C-c that expands cases into patterns if patterns [meaning the keyword] are available? What I mean is that  foo : Dec (3 ≡ 2) → ℕ; foo x = {! x  !}  will give me foo (does₁ because proof₁) = {!   !}   instead of  foo (yes proof) = {!   !}; foo (no proof) = {!   !}  and that's a bit of a hassle for a couple reasons, one of which I'm writing an issue for
 Feb 12 04:16:54 <MarcelineVQ>	I expect not since that's a rabbit-hole but am asking just in case
 Feb 12 04:56:27 <gallais>	MarcelineVQ: if you split further on proof₁ then Agda will resugar the yes/no patterns
 Feb 12 04:58:38 <MarcelineVQ>	hmm so it will, that's interesting thank you
	Feb 12 04:14:47 <MarcelineVQ> gallais: is there a C-c C-c that expands cases into patterns if patterns [meaning the keyword] are available? What I mean is that foo : Dec (3 ≡ 2) → ℕ; foo x = {! x !} will give me foo (does₁ because proof₁) = {! !} instead of foo (yes proof) = {! !}; foo (no proof) = {! !} and that's a bit of a hassle for a couple reasons, one of which I'm writing an issue for
	Feb 12 04:16:54 <MarcelineVQ> I expect not since that's a rabbit-hole but am asking just in case
	Feb 12 04:56:27 <gallais> MarcelineVQ: if you split further on proof₁ then Agda will resugar the yes/no patterns
	Feb 12 04:58:38 <MarcelineVQ> hmm so it will, that's interesting thank you