beginner universe question: comparing two nats

Stream: lean4

[Michal Wallace (tangentstorm)]

I am trying to describe a data structure similar to a binary decision diagram, but for representing Boolean expressions in algebraic normal form:

-- ANF: algebraic normal form (a fully expanded sum-of-products polynomial)
-- basically a binary tree, where the V (variable) is ANDed to the HI branch,
-- and the result is XORed to the LO branch.
-- I (looks like a 1) represents "true"
-- O (looks like a 0) represents "false"
inductive ANF : Type
| I : ANF
| O : ANF
| vhl (v : nat) (hi : ANF) (lo : ANF) : ANF

def anf_not (x: ANF) : ANF :=
match x with
| ANF.I => ANF.O
| ANF.O => ANF.I
| ANF.vhl v hi lo => ANF.vhl v hi (anf_not lo)

def anf_xor (x: ANF) (y: ANF) : ANF :=
match x with
| ANF.O => y
| ANF.I => anf_not y
| ANF.vhl v1 hi1 lo1 =>
  match y with
  | ANF.O => x
  | ANF.I => anf_not x
  | ANF.vhl v2 hi2 lo2 =>
    -- construct a new node with the larger number on top
    if v1 > v2  -- <- type mismatch nat+ vs nat+1
    then  ANF.O -- just a placeholder expression
    else ANF.I -- just placeholder expression

The full error I get:

type mismatch
  v2
has type
  nat✝ : Prop
but is expected to have type
  nat✝¹ : Prop

I am aware that there is a concept called universes, but I'm surprised that I'm running into them right off the bat like this, and I have no idea what to do to fix it. Can someone help me understand what's going on here, and what to do instead?

[Matthew Ballard]

Capitalize nat

[Michal Wallace (tangentstorm)]

well... that did the trick. But why?

[Michal Wallace (tangentstorm)]

oh... i see... if it's lowercase, it's just a variable. Thanks, @Matthew Ballard !

[Matthew Ballard]

Lean doesn't know what nat is and tries to make something up for it.

[Matthew Ballard]

set_option autoImplicit false will make it error instead

[Matthew Ballard]

And tell you the underlying issue is that nat is not defined