mwleeds / epigram

Automatically exported from code.google.com/p/epigram
0 stars 0 forks source link

Demo: indentation in definitions #93

Open GoogleCodeExporter opened 8 years ago

GoogleCodeExporter commented 8 years ago
For example, the function 'compare' in Demo.pig is written as:

let compare (x : Nat)(y : Nat)(P : Nat -> Nat -> Set)(l : (x : Nat)(y : Nat) -> 
P x (plus x ('suc y)))(e : (x : Nat) -> P x x)(g : (x : Nat)(y : Nat) -> P 
(plus y ('suc x)) y) : P x y ;
<= Nat.Ind x ;
<= Nat.Ind y ;
define compare 'zero 'zero    P l e g := e 'zero ;
define compare 'zero ('suc k) P l e g := l 'zero k ;
<= Nat.Ind y ;
(...)

It would be more nicely written:

let compare (x : Nat)(y : Nat)
            (P : Nat -> Nat -> Set)
            (l : (x : Nat)(y : Nat) -> P x (plus x ('suc y)))
            (e : (x : Nat) -> P x x)
            (g : (x : Nat)(y : Nat) -> P (plus y ('suc x)) y) : P x y ;
<= Nat.Ind x ;
    <= Nat.Ind y ;
        define compare 'zero 'zero    P l e g := e 'zero ;
        define compare 'zero ('suc k) P l e g := l 'zero k ;
    <= Nat.Ind y ;
       (...)

Or something similar. Remember: spaces are stripped off, you can do whatever 
you want.

Original issue reported on code.google.com by pedag...@gmail.com on 7 Sep 2010 at 11:17

GoogleCodeExporter commented 8 years ago
...once issue 90 is dealt with, anyway.

Original comment by adamgundry on 9 Sep 2010 at 9:42