Search results

Use constants to reduce the size of translated terms

Status: Open.

#10 In sacerdot/Minimalist-Type-Theory-In-Lambda-Prolog;

· sacerdot opened on Mar 30, 2018

Rename interp_isa as interp_tau

Status: Open.

#9 In sacerdot/Minimalist-Type-Theory-In-Lambda-Prolog;

· fifofefe opened on Jan 29, 2018

tau_proof_eq for setPi does not consider the case of two non unifying functions

Status: Open.

#6 In sacerdot/Minimalist-Type-Theory-In-Lambda-Prolog;

· fifofefe opened on Nov 9, 2017

is it possible to implement tau_trasp in terms of tau (with maybe other non trivia modifications)?

Status: Open.

#5 In sacerdot/Minimalist-Type-Theory-In-Lambda-Prolog;

· fifofefe opened on Nov 9, 2017

Consider substituting dconv with conv

Status: Open.

#4 In sacerdot/Minimalist-Type-Theory-In-Lambda-Prolog;

· fifofefe opened on Nov 9, 2017

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

Status: Open.

#3 In sacerdot/Minimalist-Type-Theory-In-Lambda-Prolog;

· fifofefe opened on Jul 17, 2017