OAI/Combinatorics/UniformKServer/LiteralPartial.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.UniformKServer.LiteralVector.partial_code_exists line 13

   Source documentation

   A partial tuple-valued program compiles on every successful input.

   theorem partial_code_exists {n m : ℕ} (f : List.Vector ℕ n→.List.Vector ℕ m) (hf : Partrec f) :
       ∃c : Code,∀v w,w∈f v→w.val∈Code.eval c v.val := by
   …