All Questions
Tagged with binders type-theory
1
question
5
votes
1
answer
321
views
What is a weak function space and what does it have to do with HOAS?
What is a weak function space and what does it have to do with higher order abstract syntax?
I mean I know what a weak function space is. It's that thing you use for HOAS in Lambda Prolog or toolkits ...