Tesla Zhang‮

Also I want to avoid documenting this behavior anywhere. This is going to be used for testing and experimentation purposes _only_.

> Do you mean to disable the whole sort system, or just the level solve process? Sort system > what error should be returned if the corresponding feature(sort system/sort metavariable)...

Quoted from internal discussion > 一种是 Arend 那样的，写一坨能 parse 能 resolve 的代码，然后编译器读进去，把 concrete syntax、reference 啥的 build 好，然后把编译器里面写好的 reduction rule 放进去或者在 normalize 的算法里面特殊处理这些函数的 application > > 一种是 Agda/Rust 那样的，提供一种 pragma 一样的机制，在代码里面通过一些额外的注解（注解本身是编译器特殊处理的）来告诉编译器『please...

The second question is how should it look like. I hate the Agda and GHC approach because pragma has their semantics, why are we reusing comment syntax! I'm suggesting three...

Well, I think the vote is not good enough. Let me change it. Pragmas should be: /|Definitions|Modifiers :---:|:---:|:---: Prefixed by a token|:rocket:|:tada: Surrounded by pairs of tokens|:heart:|:smile:

You are. There are natural number literals, which corresponds to builtin natural types. I think we could automagically recognize the natural-like structures and turn them into primitive numbers at runtime.

> I think it should be a definition as it is a complete term. I think a better practice would be adding a modifier to `_+_`.

No idea why Agda didn't do that 🤷🏼

+ :tada: `@pragma(parameters)` + :eyes: `#[inline(parameters)]` + :rocket: `%inline parameters` + :smile: special comments

> > + :tada: `@pragma(parameters)` > > > > + :eyes: `#[inline(parameters)]` > > > > + :rocket: `%inline parameters` > > > > + :smile: special comments > >...