agda/agda2hs

This is stars and forks stats for /agda/agda2hs repository. As of 20 Apr, 2024 this repository has 135 stars and 24 forks.

agda2hs Agda2hs is a tool for producing verified and readable Haskell code by extracting it from a (lightly annotated) Agda program. For example, the following Agda program encodes well-formed binary search trees: open import Haskell.Prelude _≤_ : {{Ord a}} → a → a → Set x ≤ y = (x <= y) ≡ True data BST (a : Set) {{@0 _ : Ord a}} (@0 lower upper : a) : Set where Leaf : (@0 pf : lower ≤ upper) → BST a lower upper Node : (x : a) (l : BST a lower x) (r : BST a x upper) → BST a lower upper {-#...