Agda thread!!1

Hey guise

Agda thread

It's like haskell but more hipster
But mixfix is an insanely powerful tool.

I have tried reading about Per Martin Löf's type theory but never got anywhere. After my finals I think I'll try again.

I reckon that it's not Turing complete then? It's sold as a proof assistant, what exactly is possible to do in Agda?

what's mixfix?

>>3
The if then else control structure is usually an internal primitive. In Agda, it's defined as

if_then_else : bool -> a -> b
if x then f else f' =
    case x of
        true ->
           f
        false ->
           f'

>>2
Considering how similiar it is to Haskell, i'd say similair things to Haskell.

>>4
_+_ : num -> num -> num # Forgive me, i don't know much about                  #the type system (or the comments)
x + =
   (+ x)

>>4
>>5

i couldn't understand what you meant so googled it:

The term mixfix actually refers to something more flexible than that — a mixfix operator can be seen as a sequence of alternating name parts and “holes in the expression”. A hole is where the operator’s arguments go.

_ + _ has two holes and one name part + (and is infix)
if _ then _ else _ has three name parts if, then, else and three holes (and is prefix)

seems handy

>>4
Well, I meant more of the likes of "what can be done in a language where every program is required to terminate?", especially as I don't know exactly what that would entail, moreover on a language based on Constructive Type Theory.

Reading a bit more, someone mentions that you can just hack around it by making everything bounded by a fixed amount of steps (say, 2.72 bazillion steps) and Agda can prove that it'll terminate. Which is a bit bleh but I'll buy it.