11/04/11 21:38:42.94
>>16
Agdaの機能やシンタックスはかなりCoqにも影響を与えているよね。
id: forall {A: Type}, A -> A の{}とか。
国産の定理証明器だからぜひともがんばってほしいものだが。
11/04/11 21:38:42.94
>>16
Agdaの機能やシンタックスはかなりCoqにも影響を与えているよね。
id: forall {A: Type}, A -> A の{}とか。
国産の定理証明器だからぜひともがんばってほしいものだが。