I'm trying to formalize each integer as an equivalence class of pairs of natural numbers, where the first component is the positive part, and the second component is the negative part. Definition ...

Coq, unlike many others, accepts an optional explicit parameter,which can be used to indicate the decreasing structure of a fixpoint definition. From Gallina specification, 1.3.4, Fixpoint ident ...

They seem to serve similar purposes. The one difference I've noticed so far is that while Program Fixpoint will accept a compound measure like {measure (length l1 + length l2) }, Function seems to ...

I am trying to define the Ackermann-Peters function in Coq, and I'm getting an error message that I don't understand. As you can see, I'm packaging the arguments a, b of Ackermann in a pair ab; I p...

I have the following definition for terms : Inductive term : Type := | Var : variable -> term | Func : function_symbol -> list term -> term. and a function pos_list taking a list of t...

http://docs.idris-lang.org/en/v0.99/tutorial/theorems.html#totality-checking-issues states that: Secondly, the current implementation has had limited effort put into it so far, so there may stil...

What are sized types in Agda? I've tried to read the paper about MiniAgda, but failed to proceed due to the following points: Why are data types generic over their size? As far as I know the size...

is there anything like the tactic simpl for Program Fixpoints? In particular, how can one proof the following trivial statement? Program Fixpoint bla (n:nat) {measure n} := match n with | 0 =&g...

I'm trying to define the game inductive type for combinatorial games. I want a comparison method which tells if two games are lessOrEq, greatOrEq, lessOrConf or greatOrConf. Then I can check if two...

I am fooling around with Coq. Specifically, I am trying to implement mergesort and then prove that it works. My attempt at an implementation was: Fixpoint sort ls := match ls with | nil => nil...