tests/lean/matchunit.lean.expected.out - third_party/github.com/leanprover/lean4 - Git at Google


            
            def f : Unit → Nat :=

            
            fun a => 10

            
            def g : Unit → Unit :=

            
            fun a =>

            
              match a with

            
              | b@h:PUnit.unit => b
	def f : Unit → Nat :=
	fun a => 10
	def g : Unit → Unit :=
	fun a =>
	match a with
	\| b@h:PUnit.unit => b