Open BtheCat opened 3 years ago
For an application of coq-forcing plugin I'm working on with @herbelin, we needed a definition restricted at specific world. I added the following syntax with an optional "from" clause :
"Forcing" "Definition" ident(id) ":" lconstr(typ) "as" ident(id') "using" global(obj) global(hom) "from" constr(c)
It was useful for us and maybe it can be useful for others too. We can give more details if you want.
For an application of coq-forcing plugin I'm working on with @herbelin, we needed a definition restricted at specific world. I added the following syntax with an optional "from" clause :
It was useful for us and maybe it can be useful for others too. We can give more details if you want.