## Stream: new members

### Topic: Silly Imp problem

#### Kevin Sullivan (Aug 08 2020 at 19:05):

We've implemented a minimal imperative language following Pierce's Imp chapter. On line 28, the definition of cEval, we're getting this error: infer type failed, unknown variable _f_1. We're not familiar enough with Lean's implementation to know why we're seeing this. There is no variable _f_1 in our program.

inductive bvar : Type
| mk (n : ℕ)

def bvar_eq : bvar → bvar → bool
| (bvar.mk n1) (bvar.mk n2) := n1=n2

inductive bExpr : Type
| BLit (b: bool)
| BVar (v: bvar)

def benv := bvar → bool

def bEval : bExpr → benv → bool
| (bExpr.BLit b) i := b
| (bExpr.BVar v) i := i v

def init_benv : benv := λ v, ff

def update_benv : benv → bvar → bool → benv
| i v b := λ v2, if (bvar_eq v v2) then b else (i v2)

inductive bCmd : Type
| bAssm (v : bvar) (e : bExpr)
| bSeq (c1 c2 : bCmd)

def cEval : benv → bCmd → benv
| i0 c :=   match c with
| (bCmd.bAssm v e) := update_benv i0 v (bEval e i0)
| (bCmd.bSeq c1 c2) :=
let i1 := (cEval i0 c1) in (cEval i1 c2)
end

def myFirstProg := bCmd.bAssm (bvar.mk 0) (bExpr.BLit ff)

def newEnv := cEval init_benv myFirstProg

#eval newEnv (bvar.mk 0)


#### Mario Carneiro (Aug 08 2020 at 20:17):

The way you have written cEval makes me think you learned this from coq style. In lean you just write a definition with multiple cases

#### Mario Carneiro (Aug 08 2020 at 20:18):

def cEval : benv → bCmd → benv
| i0 (bCmd.bAssm v e) := update_benv i0 v (bEval e i0)
| i0 (bCmd.bSeq c1 c2) := cEval (cEval i0 c1) c2


@Kevin Sullivan

#### Mario Carneiro (Aug 08 2020 at 20:26):

that said, the error message is phenomenally bad to the point that I suspect there is a bug somewhere

#### Kevin Sullivan (Aug 09 2020 at 20:07):

Mario Carneiro said:

that said, the error message is phenomenally bad to the point that I suspect there is a bug somewhere

Thanks, yeah. It is Coq-style but it seemed like a wrong response nonetheless, which is what prompted me to ask. Not sure if I should file an issue?

#### Kevin Sullivan (Aug 10 2020 at 16:18):

Kevin Sullivan said:

Mario Carneiro said:

that said, the error message is phenomenally bad to the point that I suspect there is a bug somewhere

Thanks, yeah. It is Coq-style but it seemed like a wrong response nonetheless, which is what prompted me to ask. Not sure if I should file an issue?

Lean Prover repo has been archived. Doesn't seem I can post an issue. I'm probably missing something, but maybe not. Let me know. Thanks.

#### Yakov Pechersky (Aug 10 2020 at 16:26):

The community version of Lean is at https://github.com/leanprover-community/lean

#### Kevin Sullivan (Aug 10 2020 at 17:25):

Yakov Pechersky said:

The community version of Lean is at https://github.com/leanprover-community/lean

Ah, yes, thanks.

Last updated: Dec 20 2023 at 11:08 UTC