Zulip Chat Archive

Stream: new members

Topic: pattern match basics


Jiekai (Jul 19 2021 at 02:00):

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 (Jul 19 2021 at 02:01):

You should match on both things at the same time

Yakov Pechersky (Jul 19 2021 at 02:02):

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 (Jul 19 2021 at 02:03):

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


Last updated: Dec 20 2023 at 11:08 UTC