conventions.md

Code Style Conventions

This document outlines the code style conventions used in the Clean project.

Standard Lean/Mathlib Conventions

We follow the standard Lean and Mathlib conventions for most formatting:

• Type annotations: Use spaces around :

  • ✅ (F : Type)
  • ❌ (F:Type)

• Assignment operator: Use spaces around :=

  • ✅ let x := 5
  • ❌ let x:=5

For more details, see:

• Mathlib style guide
• Mathlib naming conventions

Local Conventions

1. Named Parameters

We omit spaces around := in named parameters:

• ✅ (F:=F), (α:=α), (constant:=constant)
• ❌ (F := F), (α := α), (constant := constant)

2. Polynomial Multiplication

In polynomial expressions, we omit spaces around *:

• ✅ 2*a*b, a*b + c, x*y*z
• ❌ 2 * a * b, a * b + c, x * y * z

3. Exponents

Inside exponent expressions, we omit spaces around operators:

• ✅ 2^(8-o), 2^(n+1), x^(a*b)
• ❌ 2^(8 - o), 2^(n + 1), x^(a * b)