## Stream: general

### Topic: evaluating proofs?

#### Kenny Lau (Dec 12 2018 at 01:20):

@Mario Carneiro I think you said that it is possible to evaluate proofs... do you have an example? can we also break proof irrelevance? maybe have an unsound but computable non-classical.some?

#### Mario Carneiro (Dec 12 2018 at 01:21):

the axiom of choice is definitely nonconstructive

#### Mario Carneiro (Dec 12 2018 at 01:21):

You can evaluate proofs by using #reduce

#### Kenny Lau (Dec 12 2018 at 01:21):

the axiom of choice is definitely nonconstructive

even unsound?

no...

#### Mario Carneiro (Dec 12 2018 at 01:22):

wait, I don't think I understand what you are asking

#### Mario Carneiro (Dec 12 2018 at 01:22):

it's easy to compute a value if you are allowed to be wrong

#### Kenny Lau (Dec 12 2018 at 01:23):

so I want a function that reduces to 0 when given the input (⟨0, rfl⟩ : ∃ n, n = n)

Not in the VM

#### Kenny Lau (Dec 12 2018 at 01:23):

#reduce (⟨0, rfl⟩ : ∃ n, n = n) -- Exists.intro 0 (eq.refl 0)


why not?

#### Mario Carneiro (Dec 12 2018 at 01:23):

because that term has no representation in the VM

#### Mario Carneiro (Dec 12 2018 at 01:23):

it is a neutral value, a "unit"

#### Kenny Lau (Dec 12 2018 at 01:24):

so reduce is not VM?

no

#### Mario Carneiro (Dec 12 2018 at 01:24):

it is kernel reduction

#### Kenny Lau (Dec 12 2018 at 01:24):

interesting

Last updated: May 14 2021 at 06:16 UTC