lean2/tests/lean/noncomp_hott.hlean.expected.out


			
				
				
					
						
						
						
							
							
							noncomp_hott.hlean:1:0: error: invalid 'noncomputable' declarations, it can only be used in the standard library

						
						
					
				
				
					
						Reference in a new issue
					
					View git blame
					Copy permalink