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


            
            inductive LE' : Nat → Nat → Prop where

            
              | refl (n : Nat) : LE' n n


            #check LE'.refl

            
            #print LE'
	inductive LE' : Nat → Nat → Prop where
	\| refl (n : Nat) : LE' n n

	#check LE'.refl
	#print LE'