FrederickPu
FrederickPu
Right now System E is formulated as a bunch of axioms. However, I believe it would more sensible for it to be formulated as a type class such as Group....
When I run lake build on the following commit hash ``` require smt from git "https://github.com/ufmg-smite/lean-smt.git" @ "61dde7027e3c0d2db1564bc73c1471e7fd3f6457" ``` I get the following error: ``` frederick-pu@frederick-pu-IdeaPad-5-2-in-1-16AHP9:~/Downloads/LeanEuclid/.lake/packages/smt$ lake build ⚠ [5/97]...
when i run `lake exe get cache` i get the following error message: ``` info: mathlib: cloning https://github.com/leanprover-community/mathlib4.git to '.\.\.lake/packages\mathlib' info: batteries: cloning https://github.com/leanprover-community/batteries to '.\.\.lake/packages\batteries' info: Qq: cloning https://github.com/leanprover-community/quote4...
Able to process multiple commands at once using ``` { "cmds": ["theorem womp : 2 + 2 = 4 := by rfl", "#eval 0 = 2"]} ``` Also added multithreading...
When I run the following python script ```` import os import subprocess import json import time from concurrent.futures import ThreadPoolExecutor, as_completed import sys HOME_DIR = os.path.expanduser('~') DEFAULT_LAKE_PATH = f'{HOME_DIR}/.elan/bin/lake' DEFAULT_LEAN_WORKSPACE...
User can specify dynlibs when running lean repl using command line flag `lake env path/to/repl --dynlib pathtodynlib1.so pathtodynlib2.so ...` Added general interface for creating command line flags
I have a lean project that is dependent on both canonical and lean repl. But when I try to call the canonical tactic in lean repl it fails. ``` import...