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


            
            #check (fun x => x) Nat


            #check have x := Nat; x


            set_option pp.beta true


            #check (fun x => x) Nat


            #check have x := Nat; x


            set_option pp.all true


            #check (fun x => x) Nat
	#check (fun x => x) Nat

	#check have x := Nat; x

	set_option pp.beta true

	#check (fun x => x) Nat

	#check have x := Nat; x

	set_option pp.all true

	#check (fun x => x) Nat