caotic123

willing_to_kiss([], _, __) :- fail.
willing_to_kiss([[P, PLK, _] | T], X, P2) :- (P = X, member(P2, PLK)); willing_to_kiss(T, X, P2).

is_not_in_black_list(K, X, P2) :- member([X, _, BL], K), \+ member(P2, BL).

is_friend(E, P, H) :- (member([P, H], E); member([H, P], E)).

is_match(VM, _, M, F) :- willing_to_kiss(VM, M, F).

might_kiss([VM, _], [VG, __], M, F) :- is_match(VM, VG, M, F).

caotic123

#include <stdio.h>
#define Method(x, y, type) ((type)(x->methods[y] ))(x)

#pragma pack(1) 
typedef struct {
    void* space;
    void** methods;
    size_t size;
    int methods_size;
} table;

caotic123

From Coq Require Import ssreflect ssrfun ssrbool.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Require Import Coq.Arith.PeanoNat.
Require Import Coq.Init.Nat.
Require Import Coq.Lists.List.
Require Import Coq.Strings.Byte.
Require Import Arith Omega.
Require Import Coq.Arith.Even.

caotic123

From Coq Require Import ssreflect ssrfun ssrbool.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Require Import Coq.Init.Datatypes.

Definition Iso A B := exists (f : A -> B) (g : B -> A),
   forall x, f (g x) = x /\ forall y, g (f y) = y.

Theorem try : Iso True (option False).

caotic123

From Coq Require Import ssreflect ssrfun ssrbool.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Require Import Coq.Lists.List.
Require Import Coq.Arith.PeanoNat.
Require Import Coq.Arith.Compare_dec.
Require Import Coq.Arith.Div2.

caotic123

#include <iostream>
#include <functional>
#include <map>
#include <list>
#include <vector>
#include <tuple>
#include <algorithm>

struct Empyth {
    enum { isEmyth = 1 };

caotic123

import java.net.*;
import java.io.*;
import java.util.Optional;
import java.util.Timer;
import java.util.TimerTask;
import java.util.concurrent.Callable;
import java.util.concurrent.ExecutorService;
import java.util.concurrent.Executors;
import java.util.concurrent.Future;
import java.util.function.Function;

caotic123

In Agda : 
{-# OPTIONS --with-K #-} -- This is optional just be aware that overrides the option --without-K

data _≡_ {w : Set} (_x : w) : w -> Set where
  refl : _x ≡ _x

axiom_k : ∀ {A : Set} {a : A} (P : ∀ (H : a ≡ a) -> Set) (H : P refl) (E : a ≡ a) -> (P E)
axiom_k p H refl = H

In Kei :

caotic123

import java.net.*;
import java.io.*;
import java.util.LinkedList;
import java.util.Queue;
import java.util.concurrent.Callable;
import java.util.concurrent.ExecutorService;
import java.util.concurrent.Executors;
import java.util.concurrent.Future;
import java.util.function.*;

caotic123

∇R←IDENTITY N
  R←(N N)⍴(1,N⍴0)
∇

∇R←EXTENDBOTTOM MAT
  R←(((↑⍴MAT)⍴1),0)\[1]MAT
∇

∇R←EXTENDRIGHT MAT
  R←(((2⌷⍴MAT)⍴1),0)\MAT