Open fehrenbach opened 10 years ago
Test substitution in lambda case of typecheck push with known result type: > test: Pi s : * . s -> s = lambda t : * . lambda x : t . x ;
> test: Pi s : * . s -> s = lambda t : * . lambda x : t . x ;
Find a term that tests the same with inference.
Test substitution in lambda case of typecheck push with known result type:
> test: Pi s : * . s -> s = lambda t : * . lambda x : t . x ;Find a term that tests the same with inference.