nar 0.0.8

Narc, a dependently-typed programming language with dependent pattern matching
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24

//
// Created by Dependently-Typed Lambda Calculus on 2019-12-04
// id-func
// Author: ice10
//

definition id : {A : Type} -> A -> A;
clause id a = a;

definition flip : {A : Type}
   -> (A -> A -> A) -> A -> A -> A;
clause flip f a b = f b a;

definition flip' : {A B C : Type}
   -> (A -> B -> C) -> B -> A -> C;
clause flip' f a b = f b a;

definition flip''' : {A : Type}
   -> (A -> A -> A) -> A -> A -> A;
clause flip''' f a b = flip f a b;

definition flip'' : {A : Type}
   -> (A -> A -> A) -> A -> A -> A;
clause flip'' f a b = flip' f a b;