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

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions