View list elements

Stream: new members

[Quinn Culver]

I have defined this list

import Mathlib

structure Cashflow :=
(time : ℝ)
(amount : ℝ)

def CashflowSequence := List Cashflow

def cashflowExample22 : CashflowSequence :=
  (List.range 10).map (λ k => { time := k+1, amount := 1000 })

How can I view the elements of the list cashflowExample22 (to ensure I defined it correctly)?

[Damiano Testa]

Does #eval cashflowExample22 work? If CashflowSequence is an abbrev it might work.

[Damiano Testa]

Otherwise, you may have to add a deriving ToString or something similar to the definition of CashflowSequence -- depending on the actual code, something like this might work.

[Quinn Culver]

I just updated my MWE.

[Quinn Culver]

And I tried added deriving Repr to the end of the structure `Cashflow, but got error:

(kernel) invalid declaration, it uses unsafe declaration 'Real.instReprReal'Lean 4
unknown identifier 'reprCashflow✝'Lean 4
Repr.{u} (α : Type u) : Type u

[Quinn Culver]

and adding deriving ToString gives error:

default handlers have not been implemented yet, class: 'ToString' types: [Cashflow]

[Quinn Culver]

And no, #eval cashflowExample22 doesn't work.

[Eric Wieser]

you can write a Repr instance manually

[Kyle Miller]

It's got real numbers, so #eval isn't going to work here.

[Kyle Miller]

However, you can write a command to reduce the list and run norm_num on each entry.

import Mathlib

structure Cashflow :=
(time : ℝ)
(amount : ℝ)

def CashflowSequence := List Cashflow

def cashflowExample22 : CashflowSequence :=
  (List.range 10).map (λ k => { time := k+1, amount := 1000 })

section
open Lean Elab Meta Tactic
partial def reduce_list (e : Expr) : MetaM Expr := do
  let e' ← whnf e
  if e'.isAppOfArity ``List.nil 1 then
    return e'
  else if e'.isAppOfArity ``List.cons 3 then
    let tail ← reduce_list e'.appArg!
    return Expr.app e'.appFn! tail
  else
    return e
elab "reduce_list" : conv => withMainContext do
  Conv.changeLhs (← reduce_list (← Conv.getLhs))

macro "#list_norm_num " t:term : command =>
  `(command| #conv (reduce_list; norm_num [CoeT.coe, CoeHTCT.coe]) => $t)
end

#list_norm_num cashflowExample22
/-
[{ time := 1, amount := 1000 }, { time := 2, amount := 1000 }, { time := 3, amount := 1000 },
  { time := 4, amount := 1000 }, { time := 5, amount := 1000 }, { time := 6, amount := 1000 },
  { time := 7, amount := 1000 }, { time := 8, amount := 1000 }, { time := 9, amount := 1000 },
  { time := 10, amount := 1000 }]
-/

[Kyle Miller]

I told norm_num to unfold some coe functions that seemed to appear in your expression.

[Eric Wieser]

Quinn Culver said:

And I tried added deriving Repr to the end of the structure `Cashflow, but got error:

(kernel) invalid declaration, it uses unsafe declaration 'Real.instReprReal'Lean 4
unknown identifier 'reprCashflow✝'Lean 4
Repr.{u} (α : Type u) : Type u

This feels like a bug to me; deriving should automatically propagate unsafe, rather than erroring

[Eric Wieser]

Kyle Miller said:

It's got real numbers, so #eval isn't going to work here.

To elaborate on this thought for @Quinn Culver:

import Mathlib

#eval (3 : Real)
-- Real.ofCauchy (sorry /- 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, ... -/

[Eric Wieser]

Filed a bug as lean4#3498

[Quinn Culver]

What is the "sorry" doing there?

[Quinn Culver]

What does "COE" mean/stand for?

[Quinn Culver]

Eric Wieser said:

you can write a Repr instance manually

I barely understand Repr, so maybe I'm going into territory I don't belong, but what would that look like?

[Kyle Miller]

Quinn Culver said:

What does "COE" mean/stand for?

It's short for "coercion". The notation for them is the up arrow, and there's a coercion applied to k since k : Nat but the result needs to be a Real.