Skip to content

Comment on F*: A general-purpose proof-oriented programming languageparent

Comments

a rename might affect indentation

I think I need to see an example.

It happens when the indentation is established on the same line as other code, so having a rule that you need a newline to start indentation will avoid the issue. Examples from haskell:

    foo x y = do a <- something
                 pure somethingElse
Renaming `x` to `xxx` would push the indented block in and the subsequent lines would have to be indented too.

Similarly:

    foo x y = let a = something
                  b = anotherThing
              in somethingElse
Elm avoids this by requiring an newline after the `do` and `let` (if the `let` has multiple assignments).

Edit: This was brought to my attention by an Idris style guide that said: "Indent so that alpha conversion always works with a simple search and replace. In general this would mean starting a new line when starting a new level of indentation."

Thanks

AboutSource Built by g1lg1l

Hackerly is an independent reader for Hacker News, built on the public HN API. Not affiliated with Y Combinator.