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


            
            Lean.Name.mkStr (Lean.Name.mkNum `foo 2) "bla"

            
            `foo.bla

            
            Lean.Name.anonymous

            
            Lean.Name.mkNum Lean.Name.anonymous 11

            
            Lean.Name.mkNum `foo.bla 5

            
            `abc

            
            `«--->»

            
            `«2»
	Lean.Name.mkStr (Lean.Name.mkNum `foo 2) "bla"
	`foo.bla
	Lean.Name.anonymous
	Lean.Name.mkNum Lean.Name.anonymous 11
	Lean.Name.mkNum `foo.bla 5
	`abc
	`«--->»
	`«2»