我有一个Vehicle类型取决于PowerSource类型:
data PowerSource = Petrol | Pedal | Electric
data Vehicle : PowerSource -> Type where
Unicycle : Vehicle Pedal
Motorcycle : (fuel: Nat) -> Vehicle Petrol
Tram: (battery : Nat) -> Vehicle Electric
和一个功能wheels.Tram是一个未经处理的案件.
wheels : Vehicle power -> Nat
wheels Unicycle = 1
wheels Motorcycle = 2
当我检查wheelsREPL 的总数时,
:total wheels
Main.wheels is Total
因为我没有处理Tram类型wheels,我不明白怎么wheels可以总计.我误解了"总"是什么意思吗？