ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>β : Type u_2<VAR>α : Type u_5<VAR>r₁₂ : α → β → Prop<VAR>r₂₁ : β → α → Prop<VAR>hr : ∀ (a : α) (b : β), r₁₂ a b → r₂₁ b a<GOAL>Relator.LeftTotal r₁₂ → Relator.RightTotal r₂₁
<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_5<VAR>r₁₂ : α → β → Prop<VAR>r₂₃ : β → γ → Prop<VAR>r₁₃ : α → γ → Prop<VAR>hr : ∀ (a : α) (b : β) (c : γ), r₁₂ a b → r₂₃ b c → r₁₃ a c<GOAL>Relator.LeftTotal r₁₂ → Relator.LeftTotal r₂₃ → Relator.LeftTotal r₁₃
<VAR>α : Type u_5<VAR>r₁₁ : α → α → Prop<VAR>hr : ∀ (a : α), r₁₁ a a<GOAL>Relator.RightTotal r₁₁
<VAR>β : Type u_2<VAR>α : Type u_5<VAR>r₁₂ : α → β → Prop<VAR>r₂₁ : β → α → Prop<VAR>hr : ∀ (a : α) (b : β), r₁₂ a b → r₂₁ b a<GOAL>Relator.RightTotal r₁₂ → Relator.LeftTotal r₂₁
<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_5<VAR>r₁₂ : α → β → Prop<VAR>r₂₃ : β → γ → Prop<VAR>r₁₃ : α → γ → Prop<VAR>hr : ∀ (a : α) (b : β) (c : γ), r₁₂ a b → r₂₃ b c → r₁₃ a c<GOAL>Relator.RightTotal r₁₂ → Relator.RightTotal r₂₃ → Relator.RightTotal r₁₃
<VAR>α : Type u_5<VAR>r₁₁ : α → α → Prop<VAR>hr : ∀ (a : α), r₁₁ a a<GOAL>Relator.BiTotal r₁₁
<VAR>β : Type u_2<VAR>α : Type u_5<VAR>r₁₂ : α → β → Prop<VAR>r₂₁ : β → α → Prop<VAR>hr : ∀ (a : α) (b : β), r₁₂ a b → r₂₁ b a<GOAL>Relator.BiTotal r₁₂ → Relator.BiTotal r₂₁
<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_5<VAR>r₁₂ : α → β → Prop<VAR>r₂₃ : β → γ → Prop<VAR>r₁₃ : α → γ → Prop<VAR>hr : ∀ (a : α) (b : β) (c : γ), r₁₂ a b → r₂₃ b c → r₁₃ a c<GOAL>Relator.BiTotal r₁₂ → Relator.BiTotal r₂₃ → Relator.BiTotal r₁₃
<VAR>α : Type u_1<VAR>self : Encodable α<VAR>a : α<GOAL>Encodable.decode (Encodable.encode a) = some a
<VAR>α : Type u_1<VAR>Encodable α<GOAL>Function.Injective Encodable.encode
<VAR>α : Type u_1<VAR>Encodable α<VAR>a b : α<GOAL>Encodable.encode a = Encodable.encode b ↔ a = b
<VAR>α : Type u_3<VAR>Encodable α<VAR>Inhabited α<GOAL>Function.Surjective fun n => (Encodable.decode n).iget
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Encodable α<VAR>e : β ≃ α<VAR>b : β<GOAL>Encodable.encode b = Encodable.encode (e b)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Encodable α<VAR>e : β ≃ α<VAR>n : ℕ<GOAL>Encodable.decode n = Option.map (⇑e.symm) (Encodable.decode n)
<VAR>n : ℕ<GOAL>Encodable.encode n = n
<VAR>n : ℕ<GOAL>Encodable.decode n = some n
<VAR>n : ℕ<GOAL>Encodable.decode n.succ = none
<VAR>α : Type u_1<VAR>Encodable α<GOAL>Encodable.encode none = 0
<VAR>α : Type u_1<VAR>Encodable α<VAR>a : α<GOAL>Encodable.encode (some a) = (Encodable.encode a).succ
<VAR>α : Type u_1<VAR>Encodable α<GOAL>Encodable.decode 0 = some none
<VAR>α : Type u_1<VAR>Encodable α<VAR>n : ℕ<GOAL>Encodable.decode n.succ = Option.map some (Encodable.decode n)
<VAR>α : Type u_1<VAR>Encodable α<VAR>n : ℕ<VAR>a : α<GOAL>a ∈ Encodable.decode₂ α n ↔ a ∈ Encodable.decode n ∧ Encodable.encode a = n
<VAR>α : Type u_1<VAR>Encodable α<VAR>n : ℕ<VAR>a : α<GOAL>a ∈ Encodable.decode₂ α n ↔ Encodable.encode a = n
<VAR>α : Type u_1<VAR>Encodable α<VAR>n : ℕ<VAR>a : α<GOAL>Encodable.decode₂ α n = some a ↔ Encodable.encode a = n
<VAR>α : Type u_1<VAR>Encodable α<VAR>a : α<GOAL>Encodable.decode₂ α (Encodable.encode a) = some a
<VAR>α : Type u_1<VAR>Encodable α<VAR>n : ℕ<GOAL>Encodable.decode₂ α n ≠ none ↔ n ∈ Set.range Encodable.encode
<VAR>α : Type u_1<VAR>Encodable α<GOAL>Function.IsPartialInv Encodable.encode (Encodable.decode₂ α)
<VAR>α : Type u_1<VAR>Encodable α<VAR>n : ℕ<VAR>a₁ a₂ : α<VAR>h₁ : a₁ ∈ Encodable.decode₂ α n<VAR>h₂ : a₂ ∈ Encodable.decode₂ α n<GOAL>a₁ = a₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Encodable α<VAR>Encodable β<VAR>a : α<GOAL>Encodable.encode (Sum.inl a) = 2 * Encodable.encode a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Encodable α<VAR>Encodable β<VAR>b : β<GOAL>Encodable.encode (Sum.inr b) = 2 * Encodable.encode b + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Encodable α<VAR>Encodable β<VAR>n : ℕ<GOAL>Encodable.decode n = Encodable.decodeSum n
<VAR>n : ℕ<VAR>h : 2 ≤ n<GOAL>Encodable.decode n = none
<VAR>α : Type u_1<VAR>γ : α → Type u_3<VAR>Encodable α<VAR>(a : α) → Encodable (γ a)<VAR>n : ℕ<GOAL>Encodable.decode n = (Encodable.decode (Nat.unpair n).1).bind fun a => Option.map (Sigma.mk a) (Encodable.decode (Nat.unpair n).2)
<VAR>α : Type u_1<VAR>γ : α → Type u_3<VAR>Encodable α<VAR>(a : α) → Encodable (γ a)<VAR>a : α<VAR>b : γ a<GOAL>Encodable.encode ⟨a, b⟩ = Nat.pair (Encodable.encode a) (Encodable.encode b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Encodable α<VAR>Encodable β<VAR>n : ℕ<GOAL>Encodable.decode n = (Encodable.decode (Nat.unpair n).1).bind fun a => Option.map (Prod.mk a) (Encodable.decode (Nat.unpair n).2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Encodable α<VAR>Encodable β<VAR>a : α<VAR>b : β<GOAL>Encodable.encode (a, b) = Nat.pair (Encodable.encode a) (Encodable.encode b)
<VAR>α : Type u_1<VAR>P : α → Prop<VAR>encA : Encodable α<VAR>decP : DecidablePred P<VAR>a : Subtype P<GOAL>Encodable.encode a = Encodable.encode ↑a
<VAR>α : Type u_1<GOAL>Nonempty (Encodable α) ↔ Countable α
<VAR>α : Type u_1<VAR>Countable α<GOAL>Nonempty (Encodable α)
<VAR>α : Type u_1<VAR>Encodable α<VAR>a : ULower α<GOAL>ULower.down a.up = a
<VAR>α : Type u_1<VAR>Encodable α<VAR>a : α<GOAL>(ULower.down a).up = a
<VAR>α : Type u_1<VAR>Encodable α<VAR>a b : ULower α<GOAL>a.up = b.up ↔ a = b
<VAR>α : Type u_1<VAR>Encodable α<VAR>a b : α<GOAL>ULower.down a = ULower.down b ↔ a = b
<VAR>α : Type u_1<VAR>Encodable α<VAR>a b : ULower α<GOAL>a.up = b.up → a = b
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>Encodable α<VAR>DecidablePred p<VAR>h : ∃ x, p x<GOAL>p (Encodable.choose h)
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>R : (x : α) → β x → Prop<VAR>(a : α) → Encodable (β a)<VAR>(x : α) → (y : β x) → Decidable (R x y)<VAR>H : ∀ (x : α), ∃ y, R x y<GOAL>∃ f, ∀ (x : α), R x (f x)
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>P : (x : α) → β x → Prop<VAR>(a : α) → Encodable (β a)<VAR>(x : α) → (y : β x) → Decidable (P x y)<GOAL>(∀ (x : α), ∃ y, P x y) ↔ ∃ f, ∀ (x : α), P x (f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Encodable α<VAR>Inhabited α<VAR>r : β → β → Prop<VAR>f : α → β<VAR>hf : Directed r f<VAR>n : ℕ<GOAL>r (f (Directed.sequence f hf n)) (f (Directed.sequence f hf (n + 1)))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Encodable α<VAR>Inhabited α<VAR>r : β → β → Prop<VAR>f : α → β<VAR>hf : Directed r f<VAR>a : α<GOAL>r (f a) (f (Directed.sequence f hf (Encodable.encode a + 1)))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Encodable α<VAR>Inhabited α<VAR>Preorder β<VAR>f : α → β<VAR>hf : Directed (fun x x_1 => x ≤ x_1) f<GOAL>Monotone (f ∘ Directed.sequence f hf)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Encodable α<VAR>Inhabited α<VAR>Preorder β<VAR>f : α → β<VAR>hf : Directed (fun x x_1 => x ≤ x_1) f<VAR>a : α<GOAL>f a ≤ f (Directed.sequence f hf (Encodable.encode a + 1))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Encodable α<VAR>Inhabited α<VAR>Preorder β<VAR>f : α → β<VAR>hf : Directed (fun x x_1 => x ≥ x_1) f<GOAL>Antitone (f ∘ Directed.sequence f hf)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Encodable α<VAR>Inhabited α<VAR>Preorder β<VAR>f : α → β<VAR>hf : Directed (fun x x_1 => x ≥ x_1) f<VAR>a : α<GOAL>f (Directed.sequence f hf (Encodable.encode a + 1)) ≤ f a
<VAR>α : Type u_1<VAR>s : Setoid α<VAR>DecidableRel fun x x_1 => x ≈ x_1<VAR>Encodable α<VAR>q : Quotient s<GOAL>⟦q.rep⟧ = q
<VAR>f g : ℕ → ℕ<VAR>hf : Nat.Primrec f<VAR>H : ∀ (n : ℕ), f n = g n<GOAL>Nat.Primrec g
<VAR>n : ℕ<GOAL>Nat.Primrec fun x => n
<VAR>f : ℕ → ℕ<VAR>m : ℕ<VAR>hf : Nat.Primrec f<GOAL>Nat.Primrec fun n => Nat.rec m (fun y IH => f (Nat.pair y IH)) n
<VAR>f : ℕ → ℕ<VAR>m : ℕ<VAR>hf : Nat.Primrec f<GOAL>Nat.Primrec fun x => Nat.casesOn x m f
<VAR>f g : ℕ → ℕ<VAR>hf : Nat.Primrec f<VAR>hg : Nat.Primrec g<GOAL>Nat.Primrec (Nat.unpaired fun z n => Nat.casesOn n (f z) fun y => g (Nat.pair z y))
<GOAL>Nat.Primrec (Nat.unpaired (Function.swap Nat.pair))
<VAR>f : ℕ → ℕ → ℕ<VAR>hf : Nat.Primrec (Nat.unpaired f)<GOAL>Nat.Primrec (Nat.unpaired (Function.swap f))
<GOAL>Nat.Primrec (Nat.unpaired fun x x_1 => x + x_1)
<GOAL>Nat.Primrec (Nat.unpaired fun x x_1 => x - x_1)
<GOAL>Nat.Primrec (Nat.unpaired fun x x_1 => x * x_1)
<GOAL>Nat.Primrec (Nat.unpaired fun x x_1 => x ^ x_1)
<VAR>α : Type u_1<VAR>self : Primcodable α<GOAL>Nat.Primrec fun n => Encodable.encode (Encodable.decode n)
<VAR>α : Type u_1<VAR>Primcodable α<GOAL>Primrec Encodable.encode
<VAR>α : Type u_1<VAR>Primcodable α<GOAL>Primrec Encodable.decode
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>Denumerable α<VAR>Primcodable β<VAR>f : α → β<GOAL>Primrec f ↔ Nat.Primrec fun n => Encodable.encode (f (Denumerable.ofNat α n))
<VAR>f : ℕ → ℕ<GOAL>Primrec f ↔ Nat.Primrec f
<VAR>α : Type u_1<VAR>Primcodable α<GOAL>Primrec fun n => Encodable.encode (Encodable.decode n)
<VAR>α : Type u_1<VAR>Primcodable α<GOAL>Primrec some
<VAR>α : Type u_1<VAR>σ : Type u_3<VAR>Primcodable α<VAR>Primcodable σ<VAR>f g : α → σ<VAR>hf : Primrec f<VAR>H : ∀ (n : α), f n = g n<GOAL>Primrec g
<VAR>α : Type u_1<VAR>σ : Type u_3<VAR>Primcodable α<VAR>Primcodable σ<VAR>x : σ<GOAL>Primrec fun x_1 => x
<VAR>α : Type u_1<VAR>Primcodable α<GOAL>Primrec id
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_3<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable σ<VAR>f : β → σ<VAR>g : α → β<VAR>hf : Primrec f<VAR>hg : Primrec g<GOAL>Primrec fun a => f (g a)
<VAR>α : Type u_1<VAR>σ : Type u_3<VAR>Primcodable α<VAR>Primcodable σ<VAR>f : α → σ<GOAL>(Primrec fun a => Encodable.encode (f a)) ↔ Primrec f
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>Denumerable α<VAR>Primcodable β<VAR>f : α → β<GOAL>Primrec f ↔ Primrec fun n => f (Denumerable.ofNat α n)
<VAR>α : Type u_4<VAR>Denumerable α<GOAL>Primrec (Denumerable.ofNat α)
<VAR>α : Type u_1<VAR>σ : Type u_3<VAR>Primcodable α<VAR>Primcodable σ<VAR>f : α → σ<GOAL>(Primrec fun a => some (f a)) ↔ Primrec f
<VAR>α : Type u_1<VAR>Primcodable α<VAR>β : Type u_4<VAR>e : β ≃ α<GOAL>Primrec ⇑e
<VAR>α : Type u_1<VAR>Primcodable α<VAR>β : Type u_4<VAR>e : β ≃ α<GOAL>Primrec ⇑e.symm
<VAR>α : Type u_1<VAR>σ : Type u_3<VAR>Primcodable α<VAR>Primcodable σ<VAR>β : Type u_4<VAR>e : β ≃ α<VAR>f : σ → β<GOAL>(Primrec fun a => e (f a)) ↔ Primrec f
<VAR>α : Type u_1<VAR>σ : Type u_3<VAR>Primcodable α<VAR>Primcodable σ<VAR>β : Type u_4<VAR>e : β ≃ α<VAR>f : σ → α<GOAL>(Primrec fun a => e.symm (f a)) ↔ Primrec f
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Primcodable α<VAR>Primcodable β<GOAL>Primrec Prod.fst
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Primcodable α<VAR>Primcodable β<GOAL>Primrec Prod.snd
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable γ<VAR>f : α → β<VAR>g : α → γ<VAR>hf : Primrec f<VAR>hg : Primrec g<GOAL>Primrec fun a => (f a, g a)
<VAR>α : Type u_1<VAR>Primcodable α<VAR>l : List α<GOAL>Primrec l.get?
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_3<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable σ<VAR>f : α → β → σ<VAR>hf : Primrec fun p => f p.1 p.2<GOAL>Primrec₂ f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_3<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable σ<VAR>f g : α → β → σ<VAR>hg : Primrec₂ f<VAR>H : ∀ (a : α) (b : β), f a b = g a b<GOAL>Primrec₂ g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_3<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable σ<VAR>x : σ<GOAL>Primrec₂ fun x_1 x_2 => x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Primcodable α<VAR>Primcodable β<GOAL>Primrec₂ Prod.mk
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Primcodable α<VAR>Primcodable β<GOAL>Primrec₂ fun a x => a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Primcodable α<VAR>Primcodable β<GOAL>Primrec₂ fun x b => b
<VAR>α : Type u_1<VAR>Primcodable α<VAR>f : ℕ → ℕ → α<GOAL>Primrec (Nat.unpaired f) ↔ Primrec₂ f
<VAR>f : ℕ → ℕ → ℕ<GOAL>Nat.Primrec (Nat.unpaired f) ↔ Primrec₂ f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_3<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable σ<VAR>f : α → β → σ<GOAL>(Primrec₂ fun a b => Encodable.encode (f a b)) ↔ Primrec₂ f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_3<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable σ<VAR>f : α → β → σ<GOAL>(Primrec₂ fun a b => some (f a b)) ↔ Primrec₂ f
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>σ : Type u_6<VAR>Denumerable α<VAR>Denumerable β<VAR>Primcodable σ<VAR>f : α → β → σ<GOAL>Primrec₂ f ↔ Primrec₂ fun m n => f (Denumerable.ofNat α m) (Denumerable.ofNat β n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_3<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable σ<VAR>f : α → β → σ<GOAL>Primrec (Function.uncurry f) ↔ Primrec₂ f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_3<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable σ<VAR>f : α × β → σ<GOAL>Primrec₂ (Function.curry f) ↔ Primrec f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_5<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable γ<VAR>Primcodable σ<VAR>f : γ → σ<VAR>g : α → β → γ<VAR>hf : Primrec f<VAR>hg : Primrec₂ g<GOAL>Primrec₂ fun a b => f (g a b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_5<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable γ<VAR>Primcodable σ<VAR>f : β → γ → σ<VAR>g : α → β<VAR>h : α → γ<VAR>hf : Primrec₂ f<VAR>hg : Primrec g<VAR>hh : Primrec h<GOAL>Primrec fun a => f (g a) (h a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>σ : Type u_5<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable γ<VAR>Primcodable δ<VAR>Primcodable σ<VAR>f : γ → δ → σ<VAR>g : α → β → γ<VAR>h : α → β → δ<VAR>hf : Primrec₂ f<VAR>hg : Primrec₂ g<VAR>hh : Primrec₂ h<GOAL>Primrec₂ fun a b => f (g a b) (h a b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Primcodable α<VAR>Primcodable β<VAR>p : β → Prop<VAR>DecidablePred p<VAR>f : α → β<GOAL>PrimrecPred p → Primrec f → PrimrecPred fun a => p (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable γ<VAR>R : β → γ → Prop<VAR>(a : β) → (b : γ) → Decidable (R a b)<VAR>f : α → β<VAR>g : α → γ<GOAL>PrimrecRel R → Primrec f → Primrec g → PrimrecPred fun a => R (f a) (g a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable γ<VAR>Primcodable δ<VAR>R : γ → δ → Prop<VAR>(a : γ) → (b : δ) → Decidable (R a b)<VAR>f : α → β → γ<VAR>g : α → β → δ<GOAL>PrimrecRel R → Primrec₂ f → Primrec₂ g → PrimrecRel fun a b => R (f a b) (g a b)
<VAR>α : Type u_1<VAR>Primcodable α<VAR>p q : α → Prop<VAR>DecidablePred p<VAR>DecidablePred q<VAR>hp : PrimrecPred p<VAR>H : ∀ (a : α), p a ↔ q a<GOAL>PrimrecPred q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Primcodable α<VAR>Primcodable β<VAR>r s : α → β → Prop<VAR>(a : α) → (b : β) → Decidable (r a b)<VAR>(a : α) → (b : β) → Decidable (s a b)<VAR>hr : PrimrecRel r<VAR>H : ∀ (a : α) (b : β), r a b ↔ s a b<GOAL>PrimrecRel s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_3<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable σ<VAR>f : α → β → σ<VAR>h : Primrec₂ f<GOAL>Primrec₂ (Function.swap f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_3<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable σ<VAR>f : α → β → σ<GOAL>Primrec₂ f ↔ Nat.Primrec (Nat.unpaired fun m n => Encodable.encode ((Encodable.decode m).bind fun a => Option.map (f a) (Encodable.decode n)))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_3<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable σ<VAR>f : α → β → σ<GOAL>Primrec₂ f ↔ Primrec₂ fun m n => (Encodable.decode m).bind fun a => Option.map (f a) (Encodable.decode n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_5<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable σ<VAR>f : α × β → σ<VAR>hf : Primrec f<GOAL>Primrec₂ fun a b => f (a, b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Primcodable α<VAR>Primcodable β<VAR>f : α → β<VAR>g : α → ℕ × β → β<VAR>hf : Primrec f<VAR>hg : Primrec₂ g<GOAL>Primrec₂ fun a n => Nat.rec (f a) (fun n IH => g a (n, IH)) n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Primcodable α<VAR>Primcodable β<VAR>f : α → ℕ<VAR>g : α → β<VAR>h : α → ℕ × β → β<VAR>hf : Primrec f<VAR>hg : Primrec g<VAR>hh : Primrec₂ h<GOAL>Primrec fun a => Nat.rec (g a) (fun n IH => h a (n, IH)) (f a)
<VAR>α : Type u_1<VAR>Primcodable α<VAR>f : ℕ → α → α<VAR>a : α<VAR>hf : Primrec₂ f<GOAL>Primrec fun t => Nat.rec a f t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Primcodable α<VAR>Primcodable β<VAR>f : α → β<VAR>g : α → ℕ → β<VAR>hf : Primrec f<VAR>hg : Primrec₂ g<GOAL>Primrec₂ fun a n => Nat.casesOn n (f a) (g a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Primcodable α<VAR>Primcodable β<VAR>f : α → ℕ<VAR>g : α → β<VAR>h : α → ℕ → β<VAR>hf : Primrec f<VAR>hg : Primrec g<VAR>hh : Primrec₂ h<GOAL>Primrec fun a => Nat.casesOn (f a) (g a) (h a)
<VAR>α : Type u_1<VAR>Primcodable α<VAR>f : ℕ → α<VAR>a : α<VAR>hf : Primrec f<GOAL>Primrec fun n => Nat.casesOn n a f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Primcodable α<VAR>Primcodable β<VAR>f : α → ℕ<VAR>g : α → β<VAR>h : α → β → β<VAR>hf : Primrec f<VAR>hg : Primrec g<VAR>hh : Primrec₂ h<GOAL>Primrec fun a => (h a)^[f a] (g a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_5<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable σ<VAR>o : α → Option β<VAR>f : α → σ<VAR>g : α → β → σ<VAR>ho : Primrec o<VAR>hf : Primrec f<VAR>hg : Primrec₂ g<GOAL>Primrec fun a => Option.casesOn (o a) (f a) (g a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_5<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable σ<VAR>f : α → Option β<VAR>g : α → β → Option σ<VAR>hf : Primrec f<VAR>hg : Primrec₂ g<GOAL>Primrec fun a => (f a).bind (g a)
<VAR>α : Type u_1<VAR>σ : Type u_5<VAR>Primcodable α<VAR>Primcodable σ<VAR>f : α → Option σ<VAR>hf : Primrec f<GOAL>Primrec fun o => o.bind f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_5<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable σ<VAR>f : α → Option β<VAR>g : α → β → σ<VAR>hf : Primrec f<VAR>hg : Primrec₂ g<GOAL>Primrec fun a => Option.map (g a) (f a)
<VAR>α : Type u_1<VAR>σ : Type u_5<VAR>Primcodable α<VAR>Primcodable σ<VAR>f : α → σ<VAR>hf : Primrec f<GOAL>Primrec (Option.map f)
<VAR>α : Type u_1<VAR>Primcodable α<VAR>Inhabited α<GOAL>Primrec Option.iget
<VAR>α : Type u_1<VAR>Primcodable α<GOAL>Primrec Option.isSome
<VAR>α : Type u_1<VAR>Primcodable α<GOAL>Primrec₂ Option.getD
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_5<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable σ<VAR>f : α → β → Option σ<GOAL>(Primrec₂ fun a n => (Encodable.decode n).bind (f a)) ↔ Primrec₂ f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_5<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable σ<VAR>f : α → β → σ<GOAL>(Primrec₂ fun a n => Option.map (f a) (Encodable.decode n)) ↔ Primrec₂ f
<GOAL>Primrec₂ fun x x_1 => x + x_1
<GOAL>Primrec₂ fun x x_1 => x - x_1
<GOAL>Primrec₂ fun x x_1 => x * x_1
<VAR>α : Type u_1<VAR>σ : Type u_5<VAR>Primcodable α<VAR>Primcodable σ<VAR>c : α → Bool<VAR>f g : α → σ<VAR>hc : Primrec c<VAR>hf : Primrec f<VAR>hg : Primrec g<GOAL>Primrec fun a => bif c a then f a else g a
<VAR>α : Type u_1<VAR>σ : Type u_5<VAR>Primcodable α<VAR>Primcodable σ<VAR>c : α → Prop<VAR>DecidablePred c<VAR>f g : α → σ<VAR>hc : PrimrecPred c<VAR>hf : Primrec f<VAR>hg : Primrec g<GOAL>Primrec fun a => if c a then f a else g a
<GOAL>PrimrecRel fun x x_1 => x ≤ x_1
<VAR>α : Type u_1<VAR>Primcodable α<VAR>f : Bool → α<GOAL>Primrec f
<VAR>α : Type u_1<VAR>Primcodable α<VAR>f : Bool → Bool → α<GOAL>Primrec₂ f
<VAR>α : Type u_1<VAR>Primcodable α<VAR>p : α → Prop<VAR>DecidablePred p<VAR>hp : PrimrecPred p<GOAL>PrimrecPred fun a => ¬p a
<VAR>α : Type u_1<VAR>Primcodable α<VAR>p q : α → Prop<VAR>DecidablePred p<VAR>DecidablePred q<VAR>hp : PrimrecPred p<VAR>hq : PrimrecPred q<GOAL>PrimrecPred fun a => p a ∧ q a
<VAR>α : Type u_1<VAR>Primcodable α<VAR>p q : α → Prop<VAR>DecidablePred p<VAR>DecidablePred q<VAR>hp : PrimrecPred p<VAR>hq : PrimrecPred q<GOAL>PrimrecPred fun a => p a ∨ q a
<VAR>α : Type u_1<VAR>Primcodable α<VAR>DecidableEq α<GOAL>Primrec₂ BEq.beq
<VAR>α : Type u_1<VAR>Primcodable α<VAR>DecidableEq α<GOAL>PrimrecRel Eq
<GOAL>PrimrecRel fun x x_1 => x < x_1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Primcodable α<VAR>Primcodable β<VAR>p : α → β → Prop<VAR>(a : α) → (b : β) → Decidable (p a b)<VAR>hp : PrimrecRel p<VAR>f : α → β<VAR>hf : Primrec f<GOAL>Primrec fun a => Option.guard (p a) (f a)
<VAR>α : Type u_1<VAR>Primcodable α<GOAL>Primrec₂ fun x x_1 => HOrElse.hOrElse x fun x => x_1
<VAR>α : Type u_1<VAR>Primcodable α<GOAL>Primrec (Encodable.decode₂ α)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Primcodable α<VAR>Primcodable β<VAR>p : α → β → Bool<VAR>hp : Primrec₂ p<VAR>l : List β<GOAL>Primrec fun a => List.findIdx (p a) l
<VAR>α : Type u_1<VAR>Primcodable α<VAR>DecidableEq α<VAR>l : List α<GOAL>Primrec fun a => List.indexOf a l
<VAR>α : Type u_1<VAR>σ : Type u_5<VAR>Primcodable α<VAR>Primcodable σ<VAR>Finite α<VAR>f : α → σ<GOAL>Primrec f
<VAR>α : Type u_1<VAR>Primcodable α<VAR>f : α → ℕ<VAR>p : α → ℕ → Prop<VAR>(x : α) → (n : ℕ) → Decidable (p x n)<VAR>hf : Primrec f<VAR>hp : PrimrecRel p<GOAL>Primrec fun x => Nat.findGreatest (p x) (f x)
<VAR>α : Type u_1<VAR>Primcodable α<VAR>f : α → ℕ<VAR>h₁ : Primrec.PrimrecBounded f<VAR>h₂ : PrimrecRel fun a b => f a = b<GOAL>Primrec f
<GOAL>Primrec₂ fun x x_1 => x / x_1
<GOAL>Primrec₂ fun x x_1 => x % x_1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_3<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable σ<VAR>H : Nat.Primrec fun n => Encodable.encode (Encodable.decode n)<VAR>f : α → List β<VAR>g : α → σ<VAR>h : α → β × List β → σ<VAR>hf : Primrec f<VAR>hg : Primrec g<VAR>hh : Primrec₂ h<GOAL>Primrec fun a => List.casesOn (f a) (g a) fun b l => h a (b, l)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_3<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable σ<VAR>H : Nat.Primrec fun n => Encodable.encode (Encodable.decode n)<VAR>f : α → List β<VAR>g : α → σ<VAR>h : α → σ × β → σ<VAR>hf : Primrec f<VAR>hg : Primrec g<VAR>hh : Primrec₂ h<GOAL>Primrec fun a => List.foldl (fun s b => h a (s, b)) (g a) (f a)
<VAR>β : Type u_2<VAR>Primcodable β<VAR>H : Nat.Primrec fun n => Encodable.encode (Encodable.decode n)<GOAL>Primrec₂ List.cons
<VAR>β : Type u_2<VAR>Primcodable β<VAR>H : Nat.Primrec fun n => Encodable.encode (Encodable.decode n)<GOAL>Primrec List.reverse
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Primcodable α<VAR>Primcodable β<GOAL>Primrec Sum.inl
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Primcodable α<VAR>Primcodable β<GOAL>Primrec Sum.inr
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable γ<VAR>Primcodable σ<VAR>f : α → β ⊕ γ<VAR>g : α → β → σ<VAR>h : α → γ → σ<VAR>hf : Primrec f<VAR>hg : Primrec₂ g<VAR>hh : Primrec₂ h<GOAL>Primrec fun a => Sum.casesOn (f a) (g a) (h a)
<VAR>α : Type u_1<VAR>Primcodable α<GOAL>Primrec₂ List.cons
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_4<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable σ<VAR>f : α → List β<VAR>g : α → σ<VAR>h : α → β × List β → σ<GOAL>Primrec f → Primrec g → Primrec₂ h → Primrec fun a => List.casesOn (f a) (g a) fun b l => h a (b, l)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_4<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable σ<VAR>f : α → List β<VAR>g : α → σ<VAR>h : α → σ × β → σ<GOAL>Primrec f → Primrec g → Primrec₂ h → Primrec fun a => List.foldl (fun s b => h a (s, b)) (g a) (f a)
<VAR>α : Type u_1<VAR>Primcodable α<GOAL>Primrec List.reverse
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_4<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable σ<VAR>f : α → List β<VAR>g : α → σ<VAR>h : α → β × σ → σ<VAR>hf : Primrec f<VAR>hg : Primrec g<VAR>hh : Primrec₂ h<GOAL>Primrec fun a => List.foldr (fun b s => h a (b, s)) (g a) (f a)
<VAR>α : Type u_1<VAR>Primcodable α<GOAL>Primrec List.head?
<VAR>α : Type u_1<VAR>Primcodable α<VAR>Inhabited α<GOAL>Primrec List.headI
<VAR>α : Type u_1<VAR>Primcodable α<GOAL>Primrec List.tail
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_4<VAR>Primcodable α<VAR>Primcodable β<VAR>Primcodable σ<VAR>f : α → List β<VAR>g : α → σ<VAR>h : α → β × List β × σ → σ<VAR>hf : Primrec f<VAR>hg : Primrec g<VAR>hh : Primrec₂ h<GOAL>Primrec fun a => List.recOn (f a) (g a) fun b l IH => h a (b, l, IH)
<VAR>α : Type u_1<VAR>Primcodable α<GOAL>Primrec₂ List.get?
<VAR>α : Type u_1<VAR>Primcodable α<VAR>d : α<GOAL>Primrec₂ fun l n => l.getD n d
<VAR>α : Type u_1<VAR>Primcodable α<VAR>Inhabited α<GOAL>Primrec₂ List.getI
<VAR>α : Type u_1<VAR>Primcodable α<GOAL>Primrec₂ fun x x_1 => x ++ x_1
<VAR>α : Type u_1<VAR>Primcodable α<GOAL>Primrec₂ fun l a => l ++ [a]