in src/runtime/eval.ml the function check_judgement in case of Syntax.AbstractAtom _ goes to infer mode and then checks the result. This could be improved, it would be something like Syntax.Sequence except that c1 will be required to be an atom. We also have to "shave off" one layer of abstraction to the boundary and check that the atom has the required type given by the abstraction in the boundary.
in src/runtime/eval.ml the function
check_judgementin case ofSyntax.AbstractAtom _goes to infer mode and then checks the result. This could be improved, it would be something likeSyntax.Sequenceexcept thatc1will be required to be an atom. We also have to "shave off" one layer of abstraction to the boundary and check that the atom has the required type given by the abstraction in the boundary.