Zulip Chat Archive

Stream: new members

Topic: how do I define cases in a function output?


view this post on Zulip Mark Gerads (Mar 01 2021 at 08:26):

I want to define the https://www.wikiwand.com/en/Kronecker_delta on the complex numbers: it is the function which maps 0 to 1 and everything else to 0. I want it in the form def kron_del (z : ℂ) : ℂ :=, but a more general form in Mathlib might be good. Please help. :). I need it for my pet formalization project.

view this post on Zulip Jakob Scholbach (Mar 01 2021 at 08:40):

Looking at https://leanprover.github.io/introduction_to_lean/introduction_to_lean.pdf, specifically p. 29 there: you might want to try an if ... then ... else.

view this post on Zulip Eric Wieser (Mar 01 2021 at 08:40):

pi.single 0 1 z? (docs#pi.single)

view this post on Zulip Mark Gerads (Mar 01 2021 at 08:50):

def kron_del (z : ) :  := if z = 0 then 1 else 0
#eval kron_del 0

results in

code generation failed, VM does not have code for 'classical.dec_eq'

This is the first time I have seen this error.

def kron_del (z : ) :  := pi.single 0 1 z
#eval kron_del 0

results in the same error. Maybe #eval is what is broken?

view this post on Zulip Johan Commelin (Mar 01 2021 at 08:51):

@Mark Gerads try it with integers instead of complex numbers

view this post on Zulip Johan Commelin (Mar 01 2021 at 08:51):

You can't compute with arbitrary complex numbers, and hence Lean can't compute with any complex number

view this post on Zulip Mark Gerads (Mar 01 2021 at 08:56):

It works now. Thanks. I suppose I only need for the integers so far anyway.


Last updated: May 12 2021 at 05:19 UTC