New answers tagged

6

The standard well-formed-related predicate can be relatively easily extended to handle untyped PHOAS. The main subtlety is how to handle reduction at the type level. Here's a start of a two-place relation for well-typed in Coq: Require Import Coq.Lists.List. Reserved Infix "@" (left associativity, at level 11). Local Open Scope list_scope. Inductive expr ...


Top 50 recent answers are included