https://github.com/damhiya/ComputableReal/blob/master/Cauchy.agda


computable real number는 실수체계에서 계산가능한 수만을 취급하는 체계인데

그걸 agda로 쓴거임


코시수열을 조금 다루기 편하게 변형해서 정의함

원래 코시수열은 유리수 수열과 임의의 오차범위 ε에 대해서 그 오차범위를 만족하기 시작하는 인덱스 N을 주는데

이건 그냥 오차범위 ε을 만족하는 유리수를 줌.


아직 덧셈 하나 만든게 끝이라 별 대단한건 없음.. 없는데 힘들어 죽겟다