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/, 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
