argumentcomputer/yatima

Issues

• in Windows, `lake run import_all` does not work

  #281 opened 10 months ago by Seasawher
  0

• Documentation for Lean Version Upgrade

  #280 opened a year ago by agureev
  0

• Simplify the typechecker by removing lambda inference

  #272 opened 2 years ago by gabriel-barrett
  0

• Commit the typechecker as an actual lambda

  #275 opened 2 years ago by arthurpaulino
  0

• Custom override for `Std.RBMap`

  #264 opened 2 years ago by arthurpaulino
  0

• Remove thunks from the typechecker

  #268 opened 2 years ago by arthurpaulino
  0

• Can't typecheck `add_comm`

  #263 opened 2 years ago by arthurpaulino
  0

• Add a `--no-hash` flag to `prove`

  #265 opened 2 years ago by arthurpaulino
  0

• Drop `blake3`

  #250 opened 2 years ago by arthurpaulino
  0

• Refactor `Value.app` to contain complete type information

  #244 opened 2 years ago by winston-h-zhang
  0

• need new flake.nix for Poseidon dependency

  #249 opened 2 years ago by johnchandlerburnham
  0

• flake.nix is broken

  #247 opened 2 years ago by johnchandlerburnham
  0

• Constant -> Declaration

  #245 opened 2 years ago by arthurpaulino
  0

• Typechecker stack overflow

  #243 opened 2 years ago by arthurpaulino
  0

• Use a `.yatima_store`

  #200 opened 2 years ago by arthurpaulino
  0

• Optional compilation

  #201 opened 2 years ago by arthurpaulino
  0

• Refactor `ToIpld` to `ToLurk`

  #205 opened 2 years ago by winston-h-zhang
  1

• Fix typechecking with `private opaque` definitions

  #232 opened 2 years ago by rish987
  0

• [RFC] Generating Lurk proofs of typechecking

  #236 opened 2 years ago by arthurpaulino
  2

• Compiler to the EVM through Yul

  #238 opened 2 years ago by gabriel-barrett
  0

• Cache expressions in the converter

  #180 opened 2 years ago by arthurpaulino
  0

• Anonymize converter

  #222 opened 2 years ago by arthurpaulino
  0

• Anonymize transpiler

  #223 opened 2 years ago by arthurpaulino
  0

• Minimum working example.

  #228 opened 2 years ago by he-chien-tsai
  2

• Add `NatBeq` to list of ovirrides

  #220 opened 2 years ago by arthurpaulino
  0

• Invalid code generation

  #221 opened 2 years ago by arthurpaulino
  0

• Handle name clashes

  #216 opened 2 years ago by arthurpaulino
  0

• Backtrack AST dependencies and clean up

  #215 opened 2 years ago by arthurpaulino
  0

• Modularize Lurk AST simplifiers

  #214 opened 2 years ago by arthurpaulino
  0

• Double check `Yatima.Expr.isVarFree` and `Yatima.Expr.getBVars`

  #164 opened 2 years ago by arthurpaulino
  1

• Use strings for Lurk names

  #189 opened 2 years ago by arthurpaulino
  2

• Problem: The transpiler should erase types

  #152 opened 2 years ago by winston-h-zhang
  1

• Use primitive representations of `Nat/Char/String`

  #169 opened 2 years ago by winston-h-zhang
  0

• Adding proof irrelevance back

  #188 opened 2 years ago by gabriel-barrett
  0

• IPFS support

  #191 opened 2 years ago by arthurpaulino
  0

• Remove `prelude` flag from compiler options

  #198 opened 2 years ago by winston-h-zhang
  3

• Replace erased partial functions with their `_unsafe_rec` counterparts

  #194 opened 2 years ago by winston-h-zhang
  0

• Transpiling Mutuals Round 2

  #167 opened 2 years ago by winston-h-zhang
  1

• Transpile External Recursors

  #168 opened 2 years ago by winston-h-zhang
  1

• Bug on evaluator

  #175 opened 2 years ago by arthurpaulino
  0

• Add hashes to `Typechecker.Expr`

  #185 opened 2 years ago by gabriel-barrett
  0

• Write a Lurk interpreter in Lean

  #173 opened 2 years ago by winston-h-zhang
  0

• Negative typecheck tests

  #181 opened 2 years ago by arthurpaulino
  0

• Fix converter caching

  #160 opened 2 years ago by rish987
  0

• Bug when compiling multiple files

  #165 opened 2 years ago by arthurpaulino
  3

• Broken typechecker

  #176 opened 2 years ago by arthurpaulino
  0

• Experiment caching universes and expressions

  #170 opened 2 years ago by arthurpaulino
  1

• Document everything

  #158 opened 2 years ago by arthurpaulino
  0

• Integrate transpiling into the CLI

  #150 opened 2 years ago by winston-h-zhang
  1

• Add `IO` to `TranspileM`

  #154 opened 2 years ago by winston-h-zhang
  3