sp-eta-postpone/syntax.sig

PTm(VarPTm) : Type
PTag : Type
Ty : Type

Fun : Ty -> Ty -> Ty
Prod : Ty -> Ty -> Ty
Void : Ty

PL : PTag
PR : PTag

PAbs : (bind PTm in PTm) -> PTm
PApp : PTm -> PTm -> PTm
PPair : PTm -> PTm -> PTm
PProj : PTag -> PTm -> PTm
Add a mostly finished eta postponement proof 2025-01-25 16:08:21 -07:00			`PTm(VarPTm) : Type`
			`PTag : Type`
			`Ty : Type`

			`Fun : Ty -> Ty -> Ty`
			`Prod : Ty -> Ty -> Ty`
			`Void : Ty`

			`PL : PTag`
			`PR : PTag`

Add tstar to preserve eta normal forms 2025-01-27 16:44:48 -05:00			`PAbs : (bind PTm in PTm) -> PTm`
Add a mostly finished eta postponement proof 2025-01-25 16:08:21 -07:00			`PApp : PTm -> PTm -> PTm`
			`PPair : PTm -> PTm -> PTm`
			`PProj : PTag -> PTm -> PTm`