Some questions on embedding languages

[JonathanBrouwer]

Dear Lambdapi team,

My goal (as a small part of my master thesis) is to embed a CoC-like language in lambapi. One interesting feature of this language is let bindings, so terms of the form let x = v; b. Is it possible to nicely encode these in lambdapi?

Note that I want let bindings to have the semantics such that the following typechecks:

let T = Bool;
true : T

This means that something like this does not work:

symbol Let : Π (x : ty), Π (y : ty), Π (a : tm x), Π (b : tm x → tm y), tm y;
rule Let $x $y $a $b ↪ $b $a;

A secondary question is what is good reading/watching material to read to help me in embedding the rest of this language? I'm still struggling quite a bit in understanding the concepts of how to embed languages in logical frameworks

[fblanqui]

Hi Jonathan. I realize only now that your questions has been left unanswered all that time. I am sorry about that. It is probably too late now but I will still give some elements:

• You have a native let in Lambapi.
• Concerning embeddings, I advice you to read https://doi.org/10.46298/lmcs-19(1:12)2023.