tests/lean/redundantAlt.lean - third_party/github.com/leanprover/lean4 - Git at Google


            
            def f (x : Nat) : Nat :=

            
             match x with

            
             | 0 => 1

            
             | Nat.succ (Nat.succ x) => 3

            
             | 2 => 4

            
             | Nat.succ x => 5

            
             | 3 => 6
	def f (x : Nat) : Nat :=
	match x with
	\| 0 => 1
	\| Nat.succ (Nat.succ x) => 3
	\| 2 => 4
	\| Nat.succ x => 5
	\| 3 => 6