如何在Idris中使用分数？

Question

当我试图通过另一种划分一个整数，我得到以下信息：

Idris> 6/8 
Can't find implementation for Fractional Integer 

究竟是什么意思？ 如何使用Idris中的有理数？

Answer 1

Idris does not have a built-in type for rational numbers.你看到的装置的错误的信息，即(/)功能，这是Fractional界面的方法，要求它的参数是实现该接口的类型;然而，当前实现Fractional接口的唯一类型是Double：

Idris> :doc Fractional 
Interface Fractional 

Parameters: 
    ty 

Constraints: 
    Num ty 

Methods: 
    (/) : Fractional ty => ty -> ty -> ty 

     infixl 9 

     The function is Total 
    recip : Fractional ty => ty -> ty 


     The function is Total 
Implementations: 
    Fractional Double