feat: change default indent width from 4 to 2 spaces
This commit is contained in:
parent
ec3682ce15
commit
97a2198fe0
2 changed files with 25 additions and 25 deletions
|
|
@ -94,7 +94,7 @@ bracket "(" f ")"
|
|||
@[inline] def sbracket (f : Format) : Format :=
|
||||
bracket "[" f "]"
|
||||
|
||||
def defIndent := 4
|
||||
def defIndent := 2
|
||||
def defUnicode := true
|
||||
def defWidth := 120
|
||||
|
||||
|
|
|
|||
|
|
@ -16,48 +16,48 @@ id (@id Type Nat)
|
|||
fun (a : Nat) => a
|
||||
fun (a b : Nat) => a
|
||||
fun
|
||||
(a : Nat)
|
||||
(b : Bool) =>
|
||||
a
|
||||
(a : Nat)
|
||||
(b : Bool) =>
|
||||
a
|
||||
fun {a b : Nat} => a
|
||||
typeAs ({α : Type} → α → α) fun
|
||||
{α :
|
||||
Type}
|
||||
(a : α) =>
|
||||
a
|
||||
fun
|
||||
{α :
|
||||
Type}
|
||||
[inst :
|
||||
HasToString α]
|
||||
(a : α) =>
|
||||
@toString α inst a
|
||||
a
|
||||
fun
|
||||
{α :
|
||||
Type}
|
||||
[inst :
|
||||
HasToString α]
|
||||
(a : α) =>
|
||||
@toString α inst a
|
||||
(α : Type) → α
|
||||
(α β : Type) → α
|
||||
Type → Type → Type
|
||||
(α : Type) → α → α
|
||||
(α :
|
||||
Type) →
|
||||
(a : α) → a = a
|
||||
Type) →
|
||||
(a : α) → a = a
|
||||
{α : Type} → α
|
||||
{α :
|
||||
Type} →
|
||||
[inst :
|
||||
HasToString α] →
|
||||
α
|
||||
Type} →
|
||||
[inst :
|
||||
HasToString α] →
|
||||
α
|
||||
0
|
||||
1
|
||||
42
|
||||
"hi"
|
||||
{
|
||||
type :=
|
||||
Nat,
|
||||
val :=
|
||||
0 :
|
||||
PointedType }
|
||||
type :=
|
||||
Nat,
|
||||
val :=
|
||||
0 :
|
||||
PointedType }
|
||||
(1, 2, 3)
|
||||
(1, 2).fst
|
||||
1 < 2 || true
|
||||
id (fun
|
||||
(a : Nat) =>
|
||||
a) 0
|
||||
(a : Nat) =>
|
||||
a) 0
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue