Skip to main content
Code Golf

Return to Answer

deleted 9 characters in body
Source Link
Wheat Wizard ♦
Wheat Wizard ♦
  • 100k
  • 22
  • 282
  • 661

Lean, 187 176 143143 131 bytes

def q:list ℕ→bool:=λx,(by{induction x,exact[],apply(::)1,induction x_ih with h t i,exact[],cases t,exact[h],exact(h+t_hd)::i,}:list ℕ)=x

Try it online!Try it online!

A simpler version of this can be found below:

Lean, 190 185 170169 bytes

def f:ℕ→list ℕ:=λn,by{induction n,exact[],apply(::)1,induction n_ih with h t i,exact[],cases t,exact[h],exact(h+t_hd)::i,}
def g:list ℕ→bool:=λx,f(x.length)=x

Try it online!Try it online!

This version defines a helper function f which gives the \$n\$th row of pascal's triangle. From here we check if the input is equal to the \$m\$th row where \$m\$ is the length of the input.

This is the straightforward way to do things.

The shorter version rolls these two into one. Instead of doing induction on the length of the list, it just does induction on the list itself. This turns the already hairy induction into a real mess.

Lean, 187 176 143 bytes

def q:list ℕ→bool:=λx,(by{induction x,exact[],apply(::)1,induction x_ih with h t i,exact[],cases t,exact[h],exact(h+t_hd)::i,}:list ℕ)=x

Try it online!

A simpler version of this can be found below:

Lean, 190 185 170 bytes

def f:ℕ→list ℕ:=λn,by{induction n,exact[],apply(::)1,induction n_ih with h t i,exact[],cases t,exact[h],exact(h+t_hd)::i,}
def g:list ℕ→bool:=λx,f(x.length)=x

Try it online!

This version defines a helper function f which gives the \$n\$th row of pascal's triangle. From here we check if the input is equal to the \$m\$th row where \$m\$ is the length of the input.

This is the straightforward way to do things.

The shorter version rolls these two into one. Instead of doing induction on the length of the list, it just does induction on the list itself. This turns the already hairy induction into a real mess.

Lean, 187 176 143 131 bytes

def q:list ℕ→bool:=λx,by{induction x,exact[],apply(::)1,induction x_ih with h t i,exact[],cases t,exact[h],exact(h+t_hd)::i}=x

Try it online!

A simpler version of this can be found below:

Lean, 190 185 169 bytes

def f:ℕ→list ℕ:=λn,by{induction n,exact[],apply(::)1,induction n_ih with h t i,exact[],cases t,exact[h],exact(h+t_hd)::i}
def g:list ℕ→bool:=λx,f(x.length)=x

Try it online!

This version defines a helper function f which gives the \$n\$th row of pascal's triangle. From here we check if the input is equal to the \$m\$th row where \$m\$ is the length of the input.

This is the straightforward way to do things.

The shorter version rolls these two into one. Instead of doing induction on the length of the list, it just does induction on the list itself. This turns the already hairy induction into a real mess.

deleted 7 characters in body
Source Link
Wheat Wizard ♦
Wheat Wizard ♦
  • 100k
  • 22
  • 282
  • 661

Lean, 187 176 158143 bytes

def q:list ℕ→bool:=λx,(by{induction x,exact[],apply list.cons (::)1,induction x_ih with h t i,exact[],cases t,exact[h],exact list.cons(h+t_hd)::i,}:list ℕ)=x

Try it online!Try it online!

A simpler version of this can be found below:

Lean, 190 185185 170 bytes

def f:ℕ→list ℕ:=λn,by{induction n,exact[],apply list.cons (::)1,induction n_ih with h t i,exact[],cases t,exact[h],exact list.cons(h+t_hd)::i,}
def g:list ℕ→bool:=λx,f(x.length)=x

Try it online!Try it online!

This version defines a helper function f which gives the \$n\$th row of pascal's triangle. From here we check if the input is equal to the \$m\$th row where \$m\$ is the length of the input.

This is the straightforward way to do things.

The shorter version rolls these two into one. Instead of doing induction on the length of the list, it just does induction on the list itself. This turns the already hairy induction into a real mess.

Lean, 187 176 158 bytes

def q:list ℕ→bool:=λx,(by{induction x,exact[],apply list.cons 1,induction x_ih with h t i,exact[],cases t,exact[h],exact list.cons(h+t_hd)i,}:list ℕ)=x

Try it online!

A simpler version of this can be found below:

Lean, 190 185 bytes

def f:ℕ→list ℕ:=λn,by{induction n,exact[],apply list.cons 1,induction n_ih with h t i,exact[],cases t,exact[h],exact list.cons(h+t_hd)i,}
def g:list ℕ→bool:=λx,f(x.length)=x

Try it online!

This version defines a helper function f which gives the \$n\$th row of pascal's triangle. From here we check if the input is equal to the \$m\$th row where \$m\$ is the length of the input.

This is the straightforward way to do things.

The shorter version rolls these two into one. Instead of doing induction on the length of the list, it just does induction on the list itself. This turns the already hairy induction into a real mess.

Lean, 187 176 143 bytes

def q:list ℕ→bool:=λx,(by{induction x,exact[],apply(::)1,induction x_ih with h t i,exact[],cases t,exact[h],exact(h+t_hd)::i,}:list ℕ)=x

Try it online!

A simpler version of this can be found below:

Lean, 190 185 170 bytes

def f:ℕ→list ℕ:=λn,by{induction n,exact[],apply(::)1,induction n_ih with h t i,exact[],cases t,exact[h],exact(h+t_hd)::i,}
def g:list ℕ→bool:=λx,f(x.length)=x

Try it online!

This version defines a helper function f which gives the \$n\$th row of pascal's triangle. From here we check if the input is equal to the \$m\$th row where \$m\$ is the length of the input.

This is the straightforward way to do things.

The shorter version rolls these two into one. Instead of doing induction on the length of the list, it just does induction on the list itself. This turns the already hairy induction into a real mess.

added 3 characters in body
Source Link
Wheat Wizard ♦
Wheat Wizard ♦
  • 100k
  • 22
  • 282
  • 661

Lean, 187 177176 158 bytes

def q:list ℕ→bool:=λx,(by{have A:list ℕ:=by{induction x,exact[],apply list.cons 1,induction x_ih with h t i,exact[],cases t,exact[h],exact list.cons(h+t_hd)i,},exact:list A=x,}ℕ)=x

Try it online!Try it online!

A simpler version of this can be found below:

Lean, 190 185 bytes

def f:ℕ→list ℕ:=λn,by{induction n,exact[],apply list.cons 1,induction n_ih with h t i,exact[],cases t,exact[h],exact list.cons(h+t_hd)i,}
def g:list ℕ→bool:=λx,f(x.length)=x

Try it online!

This version defines a helper function f which gives the \$n\$th row of pascal's triangle. From here we check if the input is equal to the \$m\$th row where \$m\$ is the length of the input.

This is the straightforward way to do things.

The shorter version rolls these two into one. Instead of doing induction on the length of the list, it just does induction on the list itself. This turns the already hairy induction into a real mess.

Lean, 187 177 bytes

def q:list ℕ→bool:=λx,by{have A:list ℕ:=by{induction x,exact[],apply list.cons 1,induction x_ih with h t i,exact[],cases t,exact[h],exact list.cons(h+t_hd)i,},exact A=x,}

Try it online!

A simpler version of this can be found below:

Lean, 190 185 bytes

def f:ℕ→list ℕ:=λn,by{induction n,exact[],apply list.cons 1,induction n_ih with h t i,exact[],cases t,exact[h],exact list.cons(h+t_hd)i,}
def g:list ℕ→bool:=λx,f(x.length)=x

Try it online!

This version defines a helper function f which gives the \$n\$th row of pascal's triangle. From here we check if the input is equal to the \$m\$th row where \$m\$ is the length of the input.

This is the straightforward way to do things.

The shorter version rolls these two into one. Instead of doing induction on the length of the list, it just does induction on the list itself. This turns the already hairy induction into a real mess.

Lean, 187 176 158 bytes

def q:list ℕ→bool:=λx,(by{induction x,exact[],apply list.cons 1,induction x_ih with h t i,exact[],cases t,exact[h],exact list.cons(h+t_hd)i,}:list ℕ)=x

Try it online!

A simpler version of this can be found below:

Lean, 190 185 bytes

def f:ℕ→list ℕ:=λn,by{induction n,exact[],apply list.cons 1,induction n_ih with h t i,exact[],cases t,exact[h],exact list.cons(h+t_hd)i,}
def g:list ℕ→bool:=λx,f(x.length)=x

Try it online!

This version defines a helper function f which gives the \$n\$th row of pascal's triangle. From here we check if the input is equal to the \$m\$th row where \$m\$ is the length of the input.

This is the straightforward way to do things.

The shorter version rolls these two into one. Instead of doing induction on the length of the list, it just does induction on the list itself. This turns the already hairy induction into a real mess.

Golf.
Source Link
Wheat Wizard ♦
Wheat Wizard ♦
  • 100k
  • 22
  • 282
  • 661
Source Link
Wheat Wizard ♦
Wheat Wizard ♦
  • 100k
  • 22
  • 282
  • 661