diff --git a/Assets/Scripts/GlobalBehaviour.cs b/Assets/Scripts/GlobalBehaviour.cs index 33e8f2abecdb7a6b9293f30fec21130af3b7ff75..9c28beaa311fe92f9b546835e18a6fad226b0fa9 100644 --- a/Assets/Scripts/GlobalBehaviour.cs +++ b/Assets/Scripts/GlobalBehaviour.cs @@ -1,7 +1,9 @@ using Newtonsoft.Json; +using REST_JSON_API; using System.Collections; using System.Collections.Generic; using System.IO; +using System.Text.RegularExpressions; using UnityEngine; using UnityEngine.Networking; @@ -56,7 +58,8 @@ private void Awake() return; DontDestroyOnLoad(this); - PostServerConnection(); + GetScrollsfromServer(); + GetContextfromServer(); } //TODO: Move where appropiate @@ -65,13 +68,11 @@ private void Awake() static public List<REST_JSON_API.Scroll> AvailableScrolls; public static IEnumerator InitiateScrolls = IEnumeratorExtensions.yield_break; - public static FactRecorder Context = new(); - - private void PostServerConnection() + private void GetScrollsfromServer() { - StartCoroutine(InitiateScrolls = getScrollsfromServer()); + StartCoroutine(InitiateScrolls = _GetScrollsfromServer()); - IEnumerator getScrollsfromServer() + IEnumerator _GetScrollsfromServer() { //Try /scroll/listall endpoint when scroll/list is not working //UnityWebRequest request = UnityWebRequest.Get(CommunicationEvents.ServerAdress + "/scroll/listall"); @@ -133,4 +134,108 @@ IEnumerator getScrollsfromServer() yield break; } } + + public static FactRecorder Context = new(); + + private void GetContextfromServer() + { + StartCoroutine(_GetContextfromServer()); + + IEnumerator _GetContextfromServer() + { + System.DateTime requestTime = System.DateTime.UtcNow; + UnityWebRequest request = null; + for (int i = 0; i < this.tryScrollListTimes; i++) + { + request = UnityWebRequest.Get(CommunicationEvents.ServerAdress + "/fact/list"); + request.method = UnityWebRequest.kHttpVerbGET; + + yield return request.SendWebRequest(); + + if (request.result == UnityWebRequest.Result.ConnectionError + || request.result == UnityWebRequest.Result.ProtocolError) + { + Debug.LogWarning(request.error); + Debug.Log("GET /fact/list failed. Attempt: " + (i + 1).ToString()); + } + else + break; + } + System.DateTime answerTime = System.DateTime.UtcNow; + + string jsonString = null; + + if (request.result == UnityWebRequest.Result.ConnectionError + || request.result == UnityWebRequest.Result.ProtocolError) + { + Debug.LogWarning(request.error); + } + else + { + CommunicationEvents.ServerRunning = true; + + while (!request.downloadHandler.isDone) + yield return null; + jsonString = request.downloadHandler.text; + } + + if (string.IsNullOrEmpty(jsonString) + || jsonString.Equals("[]")) + { + jsonString = File.ReadAllText(Application.streamingAssetsPath + "/context.json"); + Debug.Log("Using Fallback Context: \n" + jsonString); + } + + System.DateTime parseTime = System.DateTime.UtcNow; + MMTFact[] context_facts = JsonConvert.DeserializeObject<MMTFact[]>(jsonString); + System.DateTime parseEnd = System.DateTime.UtcNow; + + System.DateTime justParseTime = default; + System.DateTime justAddinTime = default; + + bool samestep = false; + foreach (MMTFact fact in context_facts) + { + if (Regex.IsMatch(fact.@ref.uri, ".*fact\\d+$") // one of ours + || Regex.IsMatch(fact.@ref.uri, ".*SituationTheory\\d+\\?.*") // one of ours + || fact.GetDefines() == null) // Scala rule? + continue; + + List<Fact> new_list = new(); + + System.DateTime parse_time = System.DateTime.Now; + yield return ParsingDictionary.parseFactDictionary[fact.getType()](new_list, fact); + justParseTime += System.DateTime.Now - parse_time; + + if (new_list.Count == 0) + { + Debug.LogWarning("Parsing on context-fact returned empty List -> One of the dependent facts does not exist or parsing failed"); + continue; + } + + System.DateTime addin_time = System.DateTime.Now; + foreach (Fact new_fact in new_list) + { + Context.Add(new_fact, out bool exists, samestep, null, null, true, true); + if (!exists) + samestep = true; + + yield return null; + } + justAddinTime += System.DateTime.Now - addin_time; + } + + Debug.Log( + $"Context Times:\n" + + $"Summ\t{(System.DateTime.UtcNow - requestTime).TotalMilliseconds}ms\n" + + $"Server\t{(answerTime - requestTime).TotalMilliseconds}ms\n" + + $"Download\t{(parseTime - answerTime).TotalMilliseconds}ms\n" + + $"Parsing\t{(parseEnd - parseTime).TotalMilliseconds}ms\n" + + $"FactParsing\t{justParseTime.Millisecond}ms\n" + + $"FactAdding\t{justAddinTime.Millisecond}ms\n" + + ""); + + yield break; + } + } } diff --git a/Assets/Scripts/InteractionEngine/FactHandling/Facts/Fact.cs b/Assets/Scripts/InteractionEngine/FactHandling/Facts/Fact.cs index cfceb1b7683f82e651950acf05c022c65560da4a..f9fe86b7c2ebbcc0c188e14be564e1a02a414761 100644 --- a/Assets/Scripts/InteractionEngine/FactHandling/Facts/Fact.cs +++ b/Assets/Scripts/InteractionEngine/FactHandling/Facts/Fact.cs @@ -15,6 +15,8 @@ public static class ParsingDictionary //TODO: docu public static Dictionary<string, Func<List<Fact>, MMTFact, IEnumerator>> parseFactDictionary = new() { + { MMTConstants.TypeType, + GeneralFact.parseFact }, { MMTConstants.Point, PointFact.parseFact }, { MMTConstants.Metric, @@ -401,6 +403,9 @@ protected virtual string generateLabel(FactRecorder name_space) public static IEnumerator parseFact(List<Fact> ret, MMTFact fact) => null; + public virtual SOMDoc GetMMTType() + => new OMS(MMTConstants.TYPE_TO_OMS[GetType()]); + /// <summary> /// Tells a <see cref="FactRecorder"/> that \ref Fact "this" no longer uses auto-generated <see cref="GetLabel"/>, but remembers current generation variable(s). /// </summary> diff --git a/Assets/Scripts/InteractionEngine/FactHandling/Facts/MMTTypes.cs b/Assets/Scripts/InteractionEngine/FactHandling/Facts/MMTTypes.cs index a2fff9bb92d9e3cb0cd50cb6b33a04fb8053149e..71206c165b3afb929e1adc7900ff1f6127d609c9 100644 --- a/Assets/Scripts/InteractionEngine/FactHandling/Facts/MMTTypes.cs +++ b/Assets/Scripts/InteractionEngine/FactHandling/Facts/MMTTypes.cs @@ -7,6 +7,8 @@ using System.Runtime.CompilerServices; using Newtonsoft.Json; using System.Collections; +using System.Linq.Expressions; +using Newtonsoft.Json.Linq; /// <summary> /// @@ -141,11 +143,14 @@ protected override Fact _ReInitializeMe(Dictionary<string, string> old_to_new) } public override MMTFact MakeMMTDeclaration() - => new MMTGeneralFact(_LastLabel, ListType, Defines()); + => new MMTGeneralFact(_LastLabel, GetMMTType(), Defines()); public override SOMDoc Defines() => SOMDoc.MakeShallowList(payload); + public override SOMDoc GetMMTType() + => ListType; + protected override string[] GetDependentFactIds() => lids.Where(lid => lid != null).ToArray(); @@ -467,11 +472,14 @@ public static List<Fact> MMTFactory(object payload, SOMDoc indirect_payload, SOM public override MMTFact MakeMMTDeclaration() => Defines() == null ? throw new NotSupportedException(nameof(indirect_payload) + " must not be null") - : new MMTGeneralFact(_LastLabel, TupleType, Defines()); + : new MMTGeneralFact(_LastLabel, GetMMTType(), Defines()); public override SOMDoc Defines() => indirect_payload; + public override SOMDoc GetMMTType() + => TupleType; + public new static IEnumerator parseFact(List<Fact> ret, MMTFact fact) { if (fact is not MMTGeneralFact MMTSymbol) @@ -572,6 +580,9 @@ public override MMTFact MakeMMTDeclaration() public override SOMDoc Defines() => new OMLIT<float>(value); + public override SOMDoc GetMMTType() + => new OMS(MMTConstants.RealLit); + protected override bool EquivalentWrapped(RealLitFact f1, RealLitFact f2) => Mathf.Approximately(f1.value, f2.value); @@ -582,4 +593,51 @@ protected override void RecalculateTransform() { } protected override Fact _ReInitializeMe(Dictionary<string, string> old_to_new) => new RealLitFact(value); +} + +public class GeneralFact : FactWrappedCRTP<GeneralFact> +{ + public MMTFact Raw { get; private set; } + + //[JsonIgnore] + //public LambdaExpression GeneratedExpression { get; private set; } + + public GeneralFact() : base() { } + public GeneralFact(MMTFact Raw) : base() + { + this.Raw = Raw; + } + public GeneralFact(MMTFact Raw, SOMDoc ServerDefinition) : base() + { + this.Raw = Raw; + this.ServerDefinition = ServerDefinition; + } + + public new static IEnumerator parseFact(List<Fact> ret, MMTFact fact) + { + ret.Add(new GeneralFact(fact, fact.@ref)); + yield break; + } + + public override MMTFact MakeMMTDeclaration() + => Raw; + + public override SOMDoc Defines() + => Raw.GetDefines(); + + public override SOMDoc GetMMTType() + => Raw.GetMMTType() is OMS omsType && omsType.uri == MMTConstants.TypeType + ? Raw.GetDefines() + : Raw.GetMMTType(); + + protected override bool EquivalentWrapped(GeneralFact f1, GeneralFact f2) + => MMTFact.Equivalent(f1.Raw, f2.Raw); + + protected override string[] GetDependentFactIds() + => Raw.GetDependentFactIds(); + + protected override void RecalculateTransform() { } + + protected override Fact _ReInitializeMe(Dictionary<string, string> old_to_new) + => new GeneralFact(Raw.MapURIs(old_to_new)); } \ No newline at end of file diff --git a/Assets/Scripts/MMTServer/CommunicationProtocoll/Endpoints.cs b/Assets/Scripts/MMTServer/CommunicationProtocoll/Endpoints.cs index 253d603921f3169baf27d451047740ce109c1852..6320f0f8373589102402695365ea7229360ce29c 100644 --- a/Assets/Scripts/MMTServer/CommunicationProtocoll/Endpoints.cs +++ b/Assets/Scripts/MMTServer/CommunicationProtocoll/Endpoints.cs @@ -92,6 +92,19 @@ public string label public abstract SOMDoc GetDefines(); public abstract MMTFact MapURIs(Dictionary<string, string> old_to_new); + + public abstract string[] GetDependentFactIds(); + + public static bool Equivalent(MMTFact f1, MMTFact f2) + => f1.Equivalent(f2); + + public bool Equivalent(MMTFact f2) + => this.getType().Equals(f2.getType()) + && EquivalentWrapped(this, f2); + + protected abstract bool EquivalentWrapped(MMTFact f1, MMTFact f2); + + public abstract SOMDoc GetMMTType(); } /// <summary>Class for facts without values, e.g. Points</summary> @@ -157,6 +170,21 @@ public override MMTFact MapURIs(Dictionary<string, string> old_to_new) => new MMTGeneralFact(@ref, label, type.MapURIs(old_to_new), defines.MapURIs(old_to_new)); public override SOMDoc GetDefines() => defines; + + public override string[] GetDependentFactIds() + => type.GetDependentFactIds().ShallowCloneAppend(defines.GetDependentFactIds()); + + protected override bool EquivalentWrapped(MMTFact f1, MMTFact f2) + { + MMTGeneralFact g1 = (MMTGeneralFact)f1; + MMTGeneralFact g2 = (MMTGeneralFact)f2; + + return g1.type.Equivalent(g2.type) + && g1.defines.Equivalent(g2.defines); + } + + public override SOMDoc GetMMTType() + => type; } /// <summary>Class for facts with values, e.g. Distances or Angles</summary> @@ -224,6 +252,23 @@ public override MMTFact MapURIs(Dictionary<string, string> old_to_new) ); public override SOMDoc GetDefines() => lhs; + + public override string[] GetDependentFactIds() + => lhs.GetDependentFactIds().ShallowCloneAppend(value.GetDependentFactIds()); + + protected override bool EquivalentWrapped(MMTFact f1, MMTFact f2) + { + MMTValueFact g1 = (MMTValueFact)f1; + MMTValueFact g2 = (MMTValueFact)f2; + + return g1.lhs.Equivalent(g2.lhs) + && g1.value.Equivalent(g2.value); + } + + public override SOMDoc GetMMTType() + { + throw new System.NotImplementedException(); + } } public class Scroll diff --git a/Assets/Scripts/MMTServer/CommunicationProtocoll/MMTConstants.cs b/Assets/Scripts/MMTServer/CommunicationProtocoll/MMTConstants.cs index a812b891e5ee900db03c1f430f1ee9cea832c196..0a95014a59149056aa456aad510aab8d99386b93 100644 --- a/Assets/Scripts/MMTServer/CommunicationProtocoll/MMTConstants.cs +++ b/Assets/Scripts/MMTServer/CommunicationProtocoll/MMTConstants.cs @@ -69,6 +69,7 @@ public static class MMTConstants public static readonly string Tuple = "http://gl.mathhub.info/MMT/LFX/Sigma?Symbols?Tuple"; public static readonly string MakeType = "http://gl.mathhub.info/MMT/LFX/Records?Symbols?Recexp"; public static readonly string MakeTypeType = "http://gl.mathhub.info/MMT/LFX/Records?Symbols?Rectype"; + public static readonly string TypeType = "http://cds.omdoc.org/urtheories?Typed?type"; public static readonly string GetField = "http://gl.mathhub.info/MMT/LFX/Records?Symbols?Getfield"; public static readonly string ListType = "http://gl.mathhub.info/MMT/LFX/Datatypes?ListSymbols?ListType"; @@ -128,6 +129,8 @@ public static class MMTConstants public static readonly IReadOnlyDictionary<string, Type> OMS_TO_TYPE = new Dictionary<string, Type>() { + { TypeType, + typeof(Type) }, { Point, typeof(Vector3) }, { Metric, diff --git a/Assets/Scripts/MMTServer/CommunicationProtocoll/SOMDocs.cs b/Assets/Scripts/MMTServer/CommunicationProtocoll/SOMDocs.cs index d696f73e7a4c9951063525b4cd6dd86c872cbbc5..f224fd7fc9af312f2bdc4d130ccd086037679b65 100644 --- a/Assets/Scripts/MMTServer/CommunicationProtocoll/SOMDocs.cs +++ b/Assets/Scripts/MMTServer/CommunicationProtocoll/SOMDocs.cs @@ -573,7 +573,7 @@ public override string[] GetDependentFactIds() protected internal override Type ToType(Type[] args, (string name, Type type)[] bound_params) { if (FactRecorder.AllFacts.TryGetValue(uri, out Fact found)) - return found.GetType(); + return found.GetMMTType().ToType(args, bound_params); if (MMTConstants.HeterogenApplication_TO_TypeOF.TryGetValue(uri, out string s_type)) { diff --git a/Assets/StreamingAssets/context.json b/Assets/StreamingAssets/context.json new file mode 100644 index 0000000000000000000000000000000000000000..4f14544b805d44cfc4ea341bc680cc9ef2340ca3 --- /dev/null +++ b/Assets/StreamingAssets/context.json @@ -0,0 +1,2943 @@ +[ + { + "ref": { + "uri": "http://mathhub.info/FrameIT/frameworld?StepUntil?stepUntil" + }, + "label": "<no label>", + "tp": { + "params": [ + { + "uri": "http://cds.omdoc.org/urtheories?Typed?type", + "kind": "OMS" + }, + { + "name": "X", + "kind": "VAR" + }, + { + "params": [ + { + "name": "X", + "kind": "VAR" + } + ], + "ret": { + "name": "X", + "kind": "VAR" + }, + "kind": "FUNTYPE" + }, + { + "params": [ + { + "name": "X", + "kind": "VAR" + } + ], + "ret": { + "uri": "http://mathhub.info/MitM/Foundation?Logic?prop", + "kind": "OMS" + }, + "kind": "FUNTYPE" + } + ], + "ret": { + "applicant": { + "uri": "http://gl.mathhub.info/MMT/LFX/Datatypes?ListSymbols?ListType", + "kind": "OMS" + }, + "arguments": [ + { + "name": "X", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + "kind": "FUNTYPE" + }, + "df": null, + "kind": "general" + }, + { + "ref": { + "uri": "http://mathhub.info/FrameIT/frameworld?IfThenElseX?ifthenelsex" + }, + "label": "<no label>", + "tp": { + "params": [ + { + "uri": "http://cds.omdoc.org/urtheories?Typed?type", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/Foundation?Logic?prop", + "kind": "OMS" + }, + { + "name": "X", + "kind": "VAR" + }, + { + "name": "X", + "kind": "VAR" + } + ], + "ret": { + "name": "X", + "kind": "VAR" + }, + "kind": "FUNTYPE" + }, + "df": null, + "kind": "general" + }, + { + "ref": { + "uri": "http://mathhub.info/FrameIT/frameworld?StepUntilX?stepUntilX" + }, + "label": "<no label>", + "tp": { + "params": [ + { + "uri": "http://cds.omdoc.org/urtheories?Typed?type", + "kind": "OMS" + }, + { + "uri": "http://cds.omdoc.org/urtheories?Typed?type", + "kind": "OMS" + }, + { + "uri": "http://cds.omdoc.org/urtheories?Typed?type", + "kind": "OMS" + }, + { + "name": "B", + "kind": "VAR" + }, + { + "name": "C", + "kind": "VAR" + }, + { + "name": "A", + "kind": "VAR" + }, + { + "params": [ + { + "name": "B", + "kind": "VAR" + }, + { + "name": "C", + "kind": "VAR" + }, + { + "name": "A", + "kind": "VAR" + } + ], + "ret": { + "name": "A", + "kind": "VAR" + }, + "kind": "FUNTYPE" + }, + { + "params": [ + { + "name": "A", + "kind": "VAR" + } + ], + "ret": { + "uri": "http://mathhub.info/MitM/Foundation?Logic?prop", + "kind": "OMS" + }, + "kind": "FUNTYPE" + } + ], + "ret": { + "applicant": { + "uri": "http://gl.mathhub.info/MMT/LFX/Datatypes?ListSymbols?ListType", + "kind": "OMS" + }, + "arguments": [ + { + "name": "A", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + "kind": "FUNTYPE" + }, + "df": null, + "kind": "general" + }, + { + "ref": { + "uri": "http://mathhub.info/FrameIT/frameworld?Walls?wall" + }, + "label": "<no label>", + "tp": { + "uri": "http://cds.omdoc.org/urtheories?Typed?type", + "kind": "OMS" + }, + "df": { + "applicant": { + "uri": "http://gl.mathhub.info/MMT/LFX/Records?Symbols?Rectype", + "kind": "OMS" + }, + "arguments": [ + { + "name": "point1", + "tp": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point", + "kind": "OMS" + }, + "df": null, + "kind": "OML" + }, + { + "name": "point2", + "tp": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point", + "kind": "OMS" + }, + "df": null, + "kind": "OML" + }, + { + "name": "point3", + "tp": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point", + "kind": "OMS" + }, + "df": null, + "kind": "OML" + }, + { + "name": "point4", + "tp": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point", + "kind": "OMS" + }, + "df": null, + "kind": "OML" + }, + { + "name": "u", + "tp": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point", + "kind": "OMS" + }, + "df": null, + "kind": "OML" + }, + { + "name": "v", + "tp": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point", + "kind": "OMS" + }, + "df": null, + "kind": "OML" + }, + { + "name": "vc", + "tp": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point", + "kind": "OMS" + }, + "df": null, + "kind": "OML" + }, + { + "name": "a", + "tp": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + "df": null, + "kind": "OML" + }, + { + "name": "b", + "tp": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + "df": null, + "kind": "OML" + }, + { + "name": "c", + "tp": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + "df": null, + "kind": "OML" + }, + { + "name": "d", + "tp": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + "df": null, + "kind": "OML" + }, + { + "name": "length", + "tp": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + "df": null, + "kind": "OML" + }, + { + "name": "norm_vec", + "tp": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point", + "kind": "OMS" + }, + "df": null, + "kind": "OML" + } + ], + "kind": "OMA" + }, + "kind": "general" + }, + { + "ref": { + "uri": "http://mathhub.info/FrameIT/frameworld?Walls?create_wall" + }, + "label": "<no label>", + "tp": { + "params": [ + { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point", + "kind": "OMS" + } + ], + "ret": { + "uri": "http://mathhub.info/FrameIT/frameworld?Walls?wall", + "kind": "OMS" + }, + "kind": "FUNTYPE" + }, + "df": { + "Wrapper": { + "kind": "FUN", + "params": [ + { + "name": "p1", + "tp": { + "applicant": { + "uri": "http://gl.mathhub.info/MMT/LFX/Sigma?Symbols?Product", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + } + ], + "kind": "OMA" + } + }, + { + "name": "p2", + "tp": { + "applicant": { + "uri": "http://gl.mathhub.info/MMT/LFX/Sigma?Symbols?Product", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + } + ], + "kind": "OMA" + } + }, + { + "name": "p3", + "tp": { + "applicant": { + "uri": "http://gl.mathhub.info/MMT/LFX/Sigma?Symbols?Product", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + } + ], + "kind": "OMA" + } + }, + { + "name": "p4", + "tp": { + "applicant": { + "uri": "http://gl.mathhub.info/MMT/LFX/Sigma?Symbols?Product", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + } + ], + "kind": "OMA" + } + } + ], + "body": { + "applicant": { + "Wrapper": { + "kind": "FUN", + "params": [ + { + "name": "vcc", + "tp": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point", + "kind": "OMS" + } + } + ], + "body": { + "applicant": { + "uri": "http://gl.mathhub.info/MMT/LFX/Records?Symbols?Recexp", + "kind": "OMS" + }, + "arguments": [ + { + "name": "point1", + "tp": null, + "df": { + "name": "p1", + "kind": "VAR" + }, + "kind": "OML" + }, + { + "name": "point2", + "tp": null, + "df": { + "name": "p2", + "kind": "VAR" + }, + "kind": "OML" + }, + { + "name": "point3", + "tp": null, + "df": { + "name": "p3", + "kind": "VAR" + }, + "kind": "OML" + }, + { + "name": "point4", + "tp": null, + "df": { + "name": "p4", + "kind": "VAR" + }, + "kind": "OML" + }, + { + "name": "u", + "tp": null, + "df": { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point_subtractI", + "kind": "OMS" + }, + "arguments": [ + { + "name": "p2", + "kind": "VAR" + }, + { + "name": "p1", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + "kind": "OML" + }, + { + "name": "v", + "tp": null, + "df": { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point_subtractI", + "kind": "OMS" + }, + "arguments": [ + { + "name": "p3", + "kind": "VAR" + }, + { + "name": "p1", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + "kind": "OML" + }, + { + "name": "vc", + "tp": null, + "df": { + "name": "vcc", + "kind": "VAR" + }, + "kind": "OML" + }, + { + "name": "a", + "tp": null, + "df": { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?xofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + "kind": "OML" + }, + { + "name": "b", + "tp": null, + "df": { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?yofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + "kind": "OML" + }, + { + "name": "c", + "tp": null, + "df": { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?zofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + "kind": "OML" + }, + { + "name": "d", + "tp": null, + "df": { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?plus_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?plus_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?xofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?xofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "p1", + "kind": "VAR" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?yofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?yofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "p1", + "kind": "VAR" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?zofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?zofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "p1", + "kind": "VAR" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + "kind": "OML" + }, + { + "name": "length", + "tp": null, + "df": { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?sqrt", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?plus_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?plus_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?xofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?xofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?yofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?yofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?zofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?zofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + "kind": "OML" + }, + { + "name": "norm_vec", + "tp": null, + "df": { + "applicant": { + "uri": "http://gl.mathhub.info/MMT/LFX/Sigma?Symbols?Tuple", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?xofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?inv_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?sqrt", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?plus_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?plus_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?xofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?xofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?yofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?yofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?zofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?zofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?yofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?inv_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?sqrt", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?plus_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?plus_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?xofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?xofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?yofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?yofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?zofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?zofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?zofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?inv_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?sqrt", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?plus_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?plus_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?xofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?xofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?yofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?yofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?zofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?zofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + "kind": "OML" + } + ], + "kind": "OMA" + } + } + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?vec_cross", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point_subtractI", + "kind": "OMS" + }, + "arguments": [ + { + "name": "p2", + "kind": "VAR" + }, + { + "name": "p1", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point_subtractI", + "kind": "OMS" + }, + "arguments": [ + { + "name": "p3", + "kind": "VAR" + }, + { + "name": "p1", + "kind": "VAR" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + } + }, + "kind": "general" + }, + { + "ref": { + "uri": "http://mathhub.info/FrameIT/frameworld?W3DBouncingScroll?stepUntil" + }, + "label": "<no label>", + "tp": { + "params": [ + { + "uri": "http://cds.omdoc.org/urtheories?Typed?type", + "kind": "OMS" + }, + { + "name": "X", + "kind": "VAR" + }, + { + "params": [ + { + "name": "X", + "kind": "VAR" + } + ], + "ret": { + "name": "X", + "kind": "VAR" + }, + "kind": "FUNTYPE" + }, + { + "params": [ + { + "name": "X", + "kind": "VAR" + } + ], + "ret": { + "uri": "http://mathhub.info/MitM/Foundation?Logic?prop", + "kind": "OMS" + }, + "kind": "FUNTYPE" + } + ], + "ret": { + "applicant": { + "uri": "http://gl.mathhub.info/MMT/LFX/Datatypes?ListSymbols?ListType", + "kind": "OMS" + }, + "arguments": [ + { + "name": "X", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + "kind": "FUNTYPE" + }, + "df": null, + "kind": "general" + }, + { + "ref": { + "uri": "http://mathhub.info/FrameIT/frameworld?W3DBouncingScroll?filter2" + }, + "label": "<no label>", + "tp": { + "params": [ + { + "applicant": { + "uri": "http://gl.mathhub.info/MMT/LFX/Datatypes?ListSymbols?ListType", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://gl.mathhub.info/MMT/LFX/Sigma?Symbols?Product", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/FrameIT/frameworld?Walls?wall", + "kind": "OMS" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + { + "params": [ + { + "applicant": { + "uri": "http://gl.mathhub.info/MMT/LFX/Sigma?Symbols?Product", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/FrameIT/frameworld?Walls?wall", + "kind": "OMS" + } + ], + "kind": "OMA" + } + ], + "ret": { + "uri": "http://mathhub.info/MitM/Foundation?Logic?prop", + "kind": "OMS" + }, + "kind": "FUNTYPE" + } + ], + "ret": { + "applicant": { + "uri": "http://gl.mathhub.info/MMT/LFX/Datatypes?ListSymbols?ListType", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://gl.mathhub.info/MMT/LFX/Sigma?Symbols?Product", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/FrameIT/frameworld?Walls?wall", + "kind": "OMS" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + "kind": "FUNTYPE" + }, + "df": null, + "kind": "general" + }, + { + "ref": { + "uri": "http://mathhub.info/FrameIT/frameworld?Triangles?wall" + }, + "label": "<no label>", + "tp": { + "uri": "http://cds.omdoc.org/urtheories?Typed?type", + "kind": "OMS" + }, + "df": { + "applicant": { + "uri": "http://gl.mathhub.info/MMT/LFX/Records?Symbols?Rectype", + "kind": "OMS" + }, + "arguments": [ + { + "name": "point1", + "tp": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point", + "kind": "OMS" + }, + "df": null, + "kind": "OML" + }, + { + "name": "point2", + "tp": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point", + "kind": "OMS" + }, + "df": null, + "kind": "OML" + }, + { + "name": "point3", + "tp": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point", + "kind": "OMS" + }, + "df": null, + "kind": "OML" + }, + { + "name": "u", + "tp": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point", + "kind": "OMS" + }, + "df": null, + "kind": "OML" + }, + { + "name": "v", + "tp": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point", + "kind": "OMS" + }, + "df": null, + "kind": "OML" + }, + { + "name": "vc", + "tp": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point", + "kind": "OMS" + }, + "df": null, + "kind": "OML" + }, + { + "name": "a", + "tp": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + "df": null, + "kind": "OML" + }, + { + "name": "b", + "tp": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + "df": null, + "kind": "OML" + }, + { + "name": "c", + "tp": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + "df": null, + "kind": "OML" + }, + { + "name": "d", + "tp": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + "df": null, + "kind": "OML" + }, + { + "name": "length", + "tp": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + "df": null, + "kind": "OML" + }, + { + "name": "norm_vec", + "tp": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point", + "kind": "OMS" + }, + "df": null, + "kind": "OML" + } + ], + "kind": "OMA" + }, + "kind": "general" + }, + { + "ref": { + "uri": "http://mathhub.info/FrameIT/frameworld?Triangles?create_wall" + }, + "label": "<no label>", + "tp": { + "params": [ + { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point", + "kind": "OMS" + } + ], + "ret": { + "uri": "http://mathhub.info/FrameIT/frameworld?Triangles?wall", + "kind": "OMS" + }, + "kind": "FUNTYPE" + }, + "df": { + "Wrapper": { + "kind": "FUN", + "params": [ + { + "name": "p1", + "tp": { + "applicant": { + "uri": "http://gl.mathhub.info/MMT/LFX/Sigma?Symbols?Product", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + } + ], + "kind": "OMA" + } + }, + { + "name": "p2", + "tp": { + "applicant": { + "uri": "http://gl.mathhub.info/MMT/LFX/Sigma?Symbols?Product", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + } + ], + "kind": "OMA" + } + }, + { + "name": "p3", + "tp": { + "applicant": { + "uri": "http://gl.mathhub.info/MMT/LFX/Sigma?Symbols?Product", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + } + ], + "kind": "OMA" + } + } + ], + "body": { + "applicant": { + "Wrapper": { + "kind": "FUN", + "params": [ + { + "name": "vcc", + "tp": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point", + "kind": "OMS" + } + } + ], + "body": { + "applicant": { + "uri": "http://gl.mathhub.info/MMT/LFX/Records?Symbols?Recexp", + "kind": "OMS" + }, + "arguments": [ + { + "name": "point1", + "tp": null, + "df": { + "name": "p1", + "kind": "VAR" + }, + "kind": "OML" + }, + { + "name": "point2", + "tp": null, + "df": { + "name": "p2", + "kind": "VAR" + }, + "kind": "OML" + }, + { + "name": "point3", + "tp": null, + "df": { + "name": "p3", + "kind": "VAR" + }, + "kind": "OML" + }, + { + "name": "u", + "tp": null, + "df": { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point_subtractI", + "kind": "OMS" + }, + "arguments": [ + { + "name": "p2", + "kind": "VAR" + }, + { + "name": "p1", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + "kind": "OML" + }, + { + "name": "v", + "tp": null, + "df": { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point_subtractI", + "kind": "OMS" + }, + "arguments": [ + { + "name": "p3", + "kind": "VAR" + }, + { + "name": "p1", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + "kind": "OML" + }, + { + "name": "vc", + "tp": null, + "df": { + "name": "vcc", + "kind": "VAR" + }, + "kind": "OML" + }, + { + "name": "a", + "tp": null, + "df": { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?xofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + "kind": "OML" + }, + { + "name": "b", + "tp": null, + "df": { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?yofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + "kind": "OML" + }, + { + "name": "c", + "tp": null, + "df": { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?zofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + "kind": "OML" + }, + { + "name": "d", + "tp": null, + "df": { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?plus_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?plus_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?xofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?xofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "p1", + "kind": "VAR" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?yofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?yofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "p1", + "kind": "VAR" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?zofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?zofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "p1", + "kind": "VAR" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + "kind": "OML" + }, + { + "name": "length", + "tp": null, + "df": { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?sqrt", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?plus_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?plus_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?xofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?xofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?yofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?yofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?zofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?zofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + "kind": "OML" + }, + { + "name": "norm_vec", + "tp": null, + "df": { + "applicant": { + "uri": "http://gl.mathhub.info/MMT/LFX/Sigma?Symbols?Tuple", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?xofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?inv_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?sqrt", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?plus_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?plus_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?xofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?xofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?yofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?yofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?zofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?zofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?yofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?inv_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?sqrt", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?plus_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?plus_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?xofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?xofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?yofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?yofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?zofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?zofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?zofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?inv_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?sqrt", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?plus_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?plus_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?xofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?xofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?yofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?yofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?times_real_lit", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?zofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?zofpoint", + "kind": "OMS" + }, + "arguments": [ + { + "name": "vcc", + "kind": "VAR" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + "kind": "OML" + } + ], + "kind": "OMA" + } + } + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?vec_cross", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point_subtractI", + "kind": "OMS" + }, + "arguments": [ + { + "name": "p2", + "kind": "VAR" + }, + { + "name": "p1", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + { + "applicant": { + "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point_subtractI", + "kind": "OMS" + }, + "arguments": [ + { + "name": "p3", + "kind": "VAR" + }, + { + "name": "p1", + "kind": "VAR" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + } + } + }, + "kind": "general" + }, + { + "ref": { + "uri": "http://mathhub.info/FrameIT/frameworld?T3DBouncingScroll?stepUntil" + }, + "label": "<no label>", + "tp": { + "params": [ + { + "uri": "http://cds.omdoc.org/urtheories?Typed?type", + "kind": "OMS" + }, + { + "name": "X", + "kind": "VAR" + }, + { + "params": [ + { + "name": "X", + "kind": "VAR" + } + ], + "ret": { + "name": "X", + "kind": "VAR" + }, + "kind": "FUNTYPE" + }, + { + "params": [ + { + "name": "X", + "kind": "VAR" + } + ], + "ret": { + "uri": "http://mathhub.info/MitM/Foundation?Logic?prop", + "kind": "OMS" + }, + "kind": "FUNTYPE" + } + ], + "ret": { + "applicant": { + "uri": "http://gl.mathhub.info/MMT/LFX/Datatypes?ListSymbols?ListType", + "kind": "OMS" + }, + "arguments": [ + { + "name": "X", + "kind": "VAR" + } + ], + "kind": "OMA" + }, + "kind": "FUNTYPE" + }, + "df": null, + "kind": "general" + }, + { + "ref": { + "uri": "http://mathhub.info/FrameIT/frameworld?T3DBouncingScroll?filter2" + }, + "label": "<no label>", + "tp": { + "params": [ + { + "applicant": { + "uri": "http://gl.mathhub.info/MMT/LFX/Datatypes?ListSymbols?ListType", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://gl.mathhub.info/MMT/LFX/Sigma?Symbols?Product", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/FrameIT/frameworld?Triangles?wall", + "kind": "OMS" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + { + "params": [ + { + "applicant": { + "uri": "http://gl.mathhub.info/MMT/LFX/Sigma?Symbols?Product", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/FrameIT/frameworld?Triangles?wall", + "kind": "OMS" + } + ], + "kind": "OMA" + } + ], + "ret": { + "uri": "http://mathhub.info/MitM/Foundation?Logic?prop", + "kind": "OMS" + }, + "kind": "FUNTYPE" + } + ], + "ret": { + "applicant": { + "uri": "http://gl.mathhub.info/MMT/LFX/Datatypes?ListSymbols?ListType", + "kind": "OMS" + }, + "arguments": [ + { + "applicant": { + "uri": "http://gl.mathhub.info/MMT/LFX/Sigma?Symbols?Product", + "kind": "OMS" + }, + "arguments": [ + { + "uri": "http://mathhub.info/MitM/Foundation?RealLiterals?real_lit", + "kind": "OMS" + }, + { + "uri": "http://mathhub.info/FrameIT/frameworld?Triangles?wall", + "kind": "OMS" + } + ], + "kind": "OMA" + } + ], + "kind": "OMA" + }, + "kind": "FUNTYPE" + }, + "df": null, + "kind": "general" + } +] \ No newline at end of file diff --git a/Assets/StreamingAssets/context.json.meta b/Assets/StreamingAssets/context.json.meta new file mode 100644 index 0000000000000000000000000000000000000000..8ce06808cad657a59a7a99be69af281452f88c33 --- /dev/null +++ b/Assets/StreamingAssets/context.json.meta @@ -0,0 +1,7 @@ +fileFormatVersion: 2 +guid: 3765333bbf970904286c7276bd1334c8 +DefaultImporter: + externalObjects: {} + userData: + assetBundleName: + assetBundleVariant: