New answers tagged reference-request
0
The problem is equivalent to online knapsack problem. Let $n$ represents the number of items. Let the knapsack has capacity $B$. Every item $i$, has value $v_i=1$ and weight $w_i=p_i$.
The offline optimal solution:
Sort the items in increasing order of their weights ($p_{\sigma(1)}\leq p_{\sigma(2)}\leq \cdots \leq p_{\sigma(n)}$ for some permutation $\...
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
