Heap property랑 Leftist tree property가 증명되는 leftist tree 생각하다가

개쉽네 ㅈ밥이네 ㅋㅋㅋㅋ 하면서 머릿속으로 컴파일까지 끝내두고서 저렇게 했더니

PriorNil is not strictly positive 라면서 totality checker가 에러 밷음;;


https://stackoverflow.com/questions/2583337/strictly-positive-in-agda

strictly positve가 대체 뭔소린가 해서 찾아봤더니 무슨 이상한거 나옴 ㅋㅋㅋㅋㅋ


해결하려면 Prior랑 Heap정의를 수정해야 하는데 어떻게 수정해야 될지 모르겠다


이거 하는 놈들은 머리가 대체 어떻게 생겨먹은건지;;

진짜 토나오게 어렵다