agda - 如何在 Agda 中排长队

Question

我需要打破这条长线:

假设 FlipH/cw/cw/flipH : ∀ (t : Tile) -> FlipH (cw (cw (flipH t))) ≡ cw (cw t)

Agda 不会接受以下任何一项:

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)

但它确实接受了这不是很理想，因为在它再次变长之前它没有给我太多的工作空间:

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

有没有一种方法可以像我们在 Haskell 中那样断行？

Answer 1

postulate 是一个 block 关键字，这意味着它被设置为在单次出现 postulate 时解析多个假设。例如:

postulate
  A : Set
  B : Set → Set

这意味着当您将 flipH/cw/cw/flipH 放在新行时，您的运气会更好。例如，您可能想写:

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