Skip to content

Push-out facts are not simplified #585

@MaZiFAU

Description

@MaZiFAU

Using FrameIT-mmt Rest-API will not simplify returned facts, but returnd entire AST. Though the AST may be desired in some cases, iff MMT is able to resolve a term, the simplified version is preferred.

For reproduction: use e.g. http://mathhub.info/FrameIT/frameworld?OppositeLen theory/Scroll via e.g. the UFrameIT-Game.

I have attached request, expected and actual answers for an application of scroll "http://mathhub.info/FrameIT/frameworld?RiverScroll"
river_request.json
apply_river_expected.json
apply_river_actual.json

The facts listed in "river_request.json" are the following (ordered), and are added using fact/add endpoint (see Rest-API). Any ?fact<#nr> are dynamic and Ids returned from the server after sending an add request.
River_1st.json
River_2nd.json
River_3rd.json
River_4th.json
River_4.5th.json
River_5th.json (angle of facts # 2,3,1 a.k.a w,x,y)

Metadata

Metadata

Assignees

No one assigned

    Labels

    bugdevelPertains to issues on the devel branchhelp wanted

    Type

    No type
    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions