Case splitting doesn't work with multiple lines definitions

[GoogleCodeExporter]

The following code

module Bug where

data Foo : Set where
  a : Foo
  b : Foo

bar : Foo → Set
bar
  X = {!!} 

gives the following when we ask for a case split on X :

bar : Foo → Set
bar
  bar a = ?
  bar b = ?

This is strongly related to issue #575
(http://code.google.com/p/agda/issues/detail?id=575)

Original issue reported on code.google.com by fafounet@gmail.com on 23 May 2014 at 12:42

[GoogleCodeExporter]

Original comment by andres.s...@gmail.com on 15 Jun 2014 at 3:38

• Added labels: Type-Defect

[GoogleCodeExporter]

The problem here is that a fix would require more elisp hacking than anyone on
the team is willing to endure. Patches are welcome.

Original comment by ulf.nor...@gmail.com on 20 Aug 2014 at 7:10

• Added labels: Priority-Medium