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


            
            example: True :=

            
              let f: {n: Nat} → Nat

            
              | _ => 0

            
              trivial