Linear Unbeauty의 확장이며, 람다 산술이 지원된다. 구체적 구현은 미룰 예정이며, 성능대신 생산성이 높아보이는데, 실제로는 내 성격상 성능쪽으로 갈것같다.
형식증명에 쓰일 언어이다.
행렬 입력 / 반환을 언커링된 Input / Output으로 처리하는, Subrootine Realationship이라는 종류의 연산이 있다만, 실제로는 흉내만 내고, 아무짓도 안한다.
Proofmood 모드에서만 쓰는 기능이다
음…