pattern match basics

Stream: new members

[Jiekai]

def is_same_nat: nat → nat → Prop :=
| nat.zero :=
  | nat.zero := true
  | nat.succ n2 := false
| nat.succ n1 := false
  | nat.zero := false
  | nat.succ n2 := false --is_same_nat n1 n2

gives error declaration 'is_same_nat' uses sorry

def is_same_nat2 (n1 : nat) (n2 : nat) : Prop :=
match n1 with
| nat.zero :=
  match n2 with
  | nat.zero := true
  | nat.succ n22 := false
  end
| nat.succ n11 :=
  match n2 with
  | nat.zero := false
  | nat.succ n22 := false
  end
end

But this seems fine.

[Yakov Pechersky]

You should match on both things at the same time

[Yakov Pechersky]

def is_same_nat: nat → nat → Prop
| nat.zero      nat.zero    := true
| (nat.succ x) (nat.succ y) := is_same_nat x y
| _ _ := false

[Yakov Pechersky]

But that is just the inductive type eq, but specialized to nat.