← All posts tagged fp

jtootf
code fp Agda
_∘_ : {A : Set}{B : A -> Set}{C : (x : A) -> B x -> Set}
      (f : {x : A}(y : B x) -> C x y)(g : (x : A) -> B x)
      (x : A) -> C x (g x)
(f ∘ g) x = f (g x)

Agda - язык простой и красивый
jtootf
math fp ? afp.sourceforge.net — The Archive of Formal Proofs is a collection of proof libraries, examples, and larger scientific developments, mechanically checked in the theorem prover Isabelle

кто-нибудь знает что-нибудь похожее для Agda? Coq? Epigram?