Hi Pedro: It is possible to define these relations in F* using inductive predicates. See this for an example: https://github.com/FStarLang/FStar/blob/master/examples/metatheory/LambdaOmega.fst#L307
Hope this helps, -Aseem. From: fstar-club <fstar-club-boun...@lists.gforge.inria.fr> On Behalf Of Pedro Barroso via fstar-club Sent: 07 October 2021 20:25 To: fstar-club@lists.gforge.inria.fr Subject: [EXTERNAL] [fstar-club] [Help] Inductive predicates Hello, good afternoon I'm doing an exercise of deeply embedding a language in F* and I'm wondering what is the idiomatic way to implement a big step semantics relation. How can we define a relation over a specific set? I saw the examples in https://fstar-lang.org/oplss2021/<https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Ffstar-lang.org%2Foplss2021%2F&data=04%7C01%7Caseemr%40microsoft.com%7C2610d38281a94fcada9208d98a2a9b9d%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637692737920773631%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=0EK1N2YQ6vKHzPFHWcuowqZ4aEy9tNN74v0TXTvVU3I%3D&reserved=0>, however, they implemented it with an interpreter with fuel. Is it possible to implement relations close to what we do in Coq, using Inductive predicates? Thank you for your assistance in this matter, Pedro
_______________________________________________ fstar-club mailing list fstar-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/fstar-club
