search

sacerdot / Minimalist-Type-Theory-In-Lambda-Prolog

An implementation in Lambda-Prolog of the Minimalist Type Theory
4 stars 3 forks source link

scrivere le "equ" come espansioni #2

Closed fifofefe closed 6 years ago

fifofefe commented 7 years ago

P (+ A B) = x\y\ (exist x'. exisst y'\ x = inl x' and y = inl y' _and P A x' y' ) or (exist x'. exisst y'\ x = inr x' and y = inr y' _and P B x' y' )