Does indent matter in cubicaltt?

[1-p]

I was looking at lectures/lecture3.ctt and wasn't too careful about indent.

It turns out the parser can only understand the first one of the following two definition (the only difference is the indent of last line):

propPi (A : U) (B : A -> U) (h : (x : A) -> isProp (B x)) :
       isProp ((x : A) -> B x) = rem
       where
       rem (f0 f1 : (x : A) -> B x) :
           Path ((x : A) -> B x) f0 f1 =
           <i> \(x : A) -> h x (f0 x) (f1 x) @ i

propPi (A : U) (B : A -> U) (h : (x : A) -> isProp (B x)) :
       isProp ((x : A) -> B x) = rem
       where
       rem (f0 f1 : (x : A) -> B x) : 
           Path ((x : A) -> B x) f0 f1 =
       <i> \(x : A) -> h x (f0 x) (f1 x) @ i

Since I didn't see anything about indent mentioned, I'm not sure if it's supposed to be like this or a bug.

[mortberg]

Yes, the grammar is indentation sensitive (just like in Haskell). I'll clarify this in the lecture notes.

[1-p]

Another thing, not really an issue but I wish to be clarified about the lectures, is that there's no polymorphism (is there?), it seems to just use a later declared definition. At first I saw two FunExt at https://github.com/mortberg/cubicaltt/blob/master/lectures/lecture1.ctt#L442-L462 I thought it allows polymorphism.

Then the two trans, one at lecture2.ctt and one at lecture3.ctt makes it really confusing when one tries to use the trans from lecture2.ctt at the end of lecture3.ctt. (lecture3 imported lecture2)

[mortberg]

I don't understand what you mean by polymorphism. There is definitely polymorphism in the sense that you can quantify over types when writing terms (so you can for example write a polymorphic length function for lists of any type). But you seem to have something else in mind?

The system currently shadows an old definition if you introduce a new one with the same name. That's what happens with funExt and trans. It is a mistake of mine to call the first thing trans though, I'll rename it when I take a pass over the lecture notes later this week.

[mortberg]

I added some comments about indentation and renamed one of the trans to compPath.