controllare che la correzione (locDef T M) |--> (locDef X T M) sia coerente

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

An implementation in Lambda-Prolog of the Minimalist Type Theory

4 stars 3 forks source link

Open fifofefe opened 7 years ago

fifofefe commented 7 years ago

è da valutare se è più oppurtuna la notazione funzionale o quella dove c'è la variabile libera esplicita