New answers tagged lambda-calculus
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
