Łukasz Czajka
Łukasz Czajka
I run "dune build" and get the following error: coqdep theories/Plugin/Hammer.v.d *** Warning: in file Hammer.v, library Hammer.Tactics.Tactics is required and has not been found in the loadpath! File "./theories/Plugin/Hammer.v",...
JuvixCore framework and evaluator. # Description JuvixCore is the Core internal representation for Juvix. It is based on a simple extended lambda-calculus, stripped down enough to enable easy compilation, but...
Depends on PR #1421 Transformations --------------------- * Lambda-lifting - Lambda-lifting a single node can be performed with umapM and the InfoTableBuilder effect. - With the current Node data structure where...
The exact scope of QuickCheck-based tests is to be determined, but they would be useful at least for the recursors to ensure that subsequent changes to the Node type do...
Depends on PR #1421 Requirements ------------------ * The translation should preserve as much information from the Internal layer as possible. - Runtime-relevant information should be translated to the Node data...
Depends on PR #1421. LetRec would be useful to implement "where" blocks and local/anonymous recursive functions.
The test fails on my machine and no hint is provided as to how to make it go through. If this is not real bug, then what should I do...
Draft of JuvixAsm # Description JuvixAsm is an abstract imperative assembly language. * Well-suited as an intermediate assembly representation for a strongly typed purely functional language with eager evaluation. *...
A common pattern in eager functional programming languages is introducing a helper tail-recursive function with additional "accumulator" arguments. The naming of this helper function is usually redundant. The helper function...
Compiling: ```agda module qs; open import Stdlib.System.IO; open import Stdlib.Data.Nat; open import Stdlib.Data.Nat.Ord; open import Stdlib.Data.List; main : IO; main := putStrLn (natToStr (length (quickSort compare (zero ∷ nil)))); end;...