Forum: >>> Magnum BBS <<<

Simple Types (Re: Class/Set distinction, was Re: 2022-10-10)

From Mild Shock@21:1/5 to Ross Finlayson on Fri Feb 23 00:32:17 2024

XPost: sci.math

I doubt that any of this fits into your squirrel brain.

For lean prover you have to first do this:

Simple Types
https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus

A formulation of the simple theory of types, Alonzo Church https://www.semanticscholar.org/paper/28bf123690205ae5bbd9f8c84b1330025e8476e4

I mean how do you want to understand a type notation like α → Prop ?

Ross Finlayson schrieb:

https://leanprover-community.github.io/mathlib_docs/set_theory/zfc/basic.html#Class

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

Sysop:	Keyop
Location:	Huddersfield, West Yorkshire, UK
Users:	741
Nodes:	16 (2 / 14)
Uptime:	86:00:11
Calls:	12,454
Calls today:	4
Files:	15,195
Messages:	6,537,809