OAI/Combinatorics/UniformKServer/LiteralVector.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.UniformKServer.LiteralVector.code_exists line 15

   Source documentation

   Compile a tuple-valued total primitive recursive map without changing its binary list interface by an additional unbounded encoding oracle.

   theorem code_exists {n m : ℕ} (f : List.Vector ℕ n→List.Vector ℕ m) (hf : Primrec f) :
       ∃c : Code,∀v,Code.eval c v.val=Part.some (f v).val := by
   …

2. def OAI.UniformKServer.LiteralVector.activeCode line 34
3. theorem OAI.UniformKServer.LiteralVector.active_eval line 35