Yu Zhang

Results 8 issues of Yu Zhang

I found the `exploit` tactic useful in case where I have `H : P -> Q` in the context or as a lemma and would like to have `Q` in...

Just a quick patch so that keywords following an underscore in identifiers won't be highlighted. For example, previously in identifier `xs_in`, the `in` gets highlighted, which is annoying. This should...

Hello, Current version of v8 supports the js-string-builtins proposal: https://github.com/WebAssembly/js-string-builtins/blob/main/proposals/js-string-builtins/Overview.md#using-builtins. To enable this feature, one needs to pass the extra argument `{ builtins: ['js-string'] }` to `Webassembly.compile`. This parameter is...

This PR implements some utilities for comparing bigints with int/int64. These utilities can be used to implement more efficient pattern matching for bigint in the compiler.

The compiler does not need `@bytes.View` to be abstract to perform optimizations. So it's changed back.

Motivation: `find_by_charcode` will be more efficient than `find_by` because it skips the surrogate pair checks. This API is used for performance-critical applications. Additionally, I'm not sure whether we want to...

## Summary This PR switched to RR backend by default. The legacy moon can be enabled by using `NEW_MOON=0`. The snapshot diffs seem to be more than expected.