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


            
            inductive Bug

            
              | mk : (Unit → Nat → Bug) → Bug