How to break long lines in Agda

user_1637329 0
Viewed 49

I need to break this long line:

postulate flipH/cw/cw/flipH : ∀ (t : Tile) -> flipH (cw (cw (flipH t))) ≡ cw (cw t)

Agda won't accept any of these:

postulate flipH/cw/cw/flipH
  : ∀ (t : Tile) -> flipH (cw (cw (flipH t))) ≡ cw (cw t)

postulate flipH/cw/cw/flipH : ∀ (t : Tile) ->
  flipH (cw (cw (flipH t))) ≡ cw (cw t)

but it does accept this which is not very ideal, since it does not give me much space to work with before it gets long again:

postulate flipH/cw/cw/flipH : ∀ (t : Tile) ->
                            flipH (cw (cw (flipH t))) ≡ cw (cw t)

Is there a way to break line similar to the way we do it in Haskell?

agda
1 Answers

postulate is a block keyword, meaning that it's set up to parse multiple postulates under a single occurrence of postulate. For example:

postulate
  A : Set
  B : Set → Set

That means you'll have better luck when you put flipH/cw/cw/flipH on a new line. For example, you might want to write:

postulate
  flipH/cw/cw/flipH : ∀ (t : Tile) ->
    flipH (cw (cw (flipH t))) ≡ cw (cw t)
user_4487960
Related