小编Ark*_*osh的帖子

我在 Idris 中将幺半群定义为

interface Is_monoid (ty : Type) (op : ty -> ty -> ty) where
    id_elem : () -> ty
    proof_of_left_id : (a : ty) -> ((op a (id_elem ())) = a)
    proof_of_right_id : (a : ty) -> ((op (id_elem ())a) = a)
    proof_of_associativity : (a, b, c : ty) -> ((op a (op b c)) = (op (op a b) c)) 

然后尝试将组定义为

interface (Is_monoid ty op) => Is_group (ty : Type) (op : ty -> ty -> ty) …

我正在一个小项目中工作,其目标是给出Gcd的定义,它给出了两个数字的gcd以及结果正确的证明.但我无法给出Gcd的完整定义.Idris 1.3.0中Gcd的定义是完全的,但是使用assert_total来强制总体性,这违背了我的项目的目的.有人有Gcd的总定义,不使用assert_total吗？

PS - 我的代码上传到 https://github.com/anotherArka/Idris-Number-Theory.git

我正在尝试使用以下代码为小语言编写解析器

import Text.ParserCombinators.Parsec
import Text.Parsec.Token

data Exp = Atom String | Op String Exp

instance Show Exp where
  show (Atom x) = x
  show (Op f x) = f ++ "(" ++ (show x) ++ ")"

parse_exp :: Parser Exp
parse_exp = (try parse_atom) <|> parse_op

parse_atom :: Parser Exp
parse_atom = do
  x <- many1 letter
  return (Atom x)

parse_op :: Parser Exp
parse_op = do
  x <- many1 letter
  char '(' 
  y <- parse_exp
  char ')'
  return (Op …